H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 5.9030000000000005 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ IFR

mainModule Main

(((^^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if n >= 0 then x ^ n else recip (x ^ (`negate` n))

is transformed to

prPr0 x n True = x ^ n

prPr0 x n False = recip (x ^ (`negate` n))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule Main

(((^^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

(((^^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

g x n

| even n

= g (x * x) (n `quot` 2)

| otherwise

= f x (n - 1) (x * y)

is transformed to

g x n = g2 x n

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g0 x n True = f x (n - 1) (x * y)

g2 x n = g1 x n (even n)

The following Function with conditions

f vv 0 y = y

f x n y =

g x n

where

g x n

| even n

= g (x * x) (n `quot` 2)

| otherwise

= f x (n - 1) (x * y)

is transformed to

f vv yu y = f4 vv yu y

f x n y = f0 x n y

f0 x n y =

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

f3 True vv yu y = y

f3 yv yw yx yy = f0 yw yx yy

f4 vv yu y = f3 (yu == 0) vv yu y

f4 yz zu zv = f0 yz zu zv

The following Function with conditions

^ x 0 = 1

^ x n

| n > 0

= f x (n - 1) x

where

f vv 0 y = y

f x n y =

g x n

where

g x n

| even n

= g (x * x) (n `quot` 2)

| otherwise

= f x (n - 1) (x * y)

^ vw vx = error []

is transformed to

^ x zy = pr4 x zy

^ x n = pr2 x n

^ vw vx = pr0 vw vx

pr0 vw vx = error []

pr2 x n =

pr1 x n (n > 0)

where

f vv yu y = f4 vv yu y

f x n y = f0 x n y

f0 x n y =

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

f3 True vv yu y = y

f3 yv yw yx yy = f0 yw yx yy

f4 vv yu y = f3 (yu == 0) vv yu y

f4 yz zu zv = f0 yz zu zv

pr1 x n True = f x (n - 1) x

pr1 x n False = pr0 x n

pr2 zw zx = pr0 zw zx

pr3 True x zy = 1

pr3 zz vuu vuv = pr2 vuu vuv

pr4 x zy = pr3 (zy == 0) x zy

pr4 vuw vux = pr2 vuw vux

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule Main

(((^^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

pr1 x n (n > 0)

where

f vv yu y = f4 vv yu y

f x n y = f0 x n y

f0 x n y =

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

f3 True vv yu y = y

f3 yv yw yx yy = f0 yw yx yy

f4 vv yu y = f3 (yu == 0) vv yu y

f4 yz zu zv = f0 yz zu zv

pr1 x n True = f x (n - 1) x

pr1 x n False = pr0 x n

are unpacked to the following functions on top level

pr2F0 x n y = pr2F0G y x n

pr2F3 True vv yu y = y

pr2F3 yv yw yx yy = pr2F0 yw yx yy

pr2F vv yu y = pr2F4 vv yu y

pr2F x n y = pr2F0 x n y

pr2Pr1 x n True = pr2F x (n - 1) x

pr2Pr1 x n False = pr0 x n

pr2F4 vv yu y = pr2F3 (yu == 0) vv yu y

pr2F4 yz zu zv = pr2F0 yz zu zv

The bindings of the following Let/Where expression

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

are unpacked to the following functions on top level

pr2F0G1 vuy x n True = pr2F0G vuy (x * x) (n `quot` 2)

pr2F0G1 vuy x n False = pr2F0G0 vuy x n otherwise

pr2F0G2 vuy x n = pr2F0G1 vuy x n (even n)

pr2F0G vuy x n = pr2F0G2 vuy x n

pr2F0G0 vuy x n True = pr2F x (n - 1) (x * vuy)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

mainModule Main

(((^^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                      ↳ Narrow

mainModule Main

((^^) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="(^^)",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="(^^) vuz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="(^^) vuz3 vuz4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="prPr0 vuz3 vuz4 (vuz4 >= fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="prPr0 vuz3 vuz4 (compare vuz4 (fromInt (Pos Zero)) /= LT)",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="prPr0 vuz3 vuz4 (not (compare vuz4 (fromInt (Pos Zero)) == LT))",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="prPr0 vuz3 vuz4 (not (primCmpInt vuz4 (fromInt (Pos Zero)) == LT))",fontsize=16,color="burlywood",shape="box"];2090[label="vuz4/Pos vuz40",fontsize=10,color="white",style="solid",shape="box"];8 -> 2090[label="",style="solid", color="burlywood", weight=9];
2090 -> 9[label="",style="solid", color="burlywood", weight=3];
2091[label="vuz4/Neg vuz40",fontsize=10,color="white",style="solid",shape="box"];8 -> 2091[label="",style="solid", color="burlywood", weight=9];
2091 -> 10[label="",style="solid", color="burlywood", weight=3];
9[label="prPr0 vuz3 (Pos vuz40) (not (primCmpInt (Pos vuz40) (fromInt (Pos Zero)) == LT))",fontsize=16,color="burlywood",shape="box"];2092[label="vuz40/Succ vuz400",fontsize=10,color="white",style="solid",shape="box"];9 -> 2092[label="",style="solid", color="burlywood", weight=9];
2092 -> 11[label="",style="solid", color="burlywood", weight=3];
2093[label="vuz40/Zero",fontsize=10,color="white",style="solid",shape="box"];9 -> 2093[label="",style="solid", color="burlywood", weight=9];
2093 -> 12[label="",style="solid", color="burlywood", weight=3];
10[label="prPr0 vuz3 (Neg vuz40) (not (primCmpInt (Neg vuz40) (fromInt (Pos Zero)) == LT))",fontsize=16,color="burlywood",shape="box"];2094[label="vuz40/Succ vuz400",fontsize=10,color="white",style="solid",shape="box"];10 -> 2094[label="",style="solid", color="burlywood", weight=9];
2094 -> 13[label="",style="solid", color="burlywood", weight=3];
2095[label="vuz40/Zero",fontsize=10,color="white",style="solid",shape="box"];10 -> 2095[label="",style="solid", color="burlywood", weight=9];
2095 -> 14[label="",style="solid", color="burlywood", weight=3];
11[label="prPr0 vuz3 (Pos (Succ vuz400)) (not (primCmpInt (Pos (Succ vuz400)) (fromInt (Pos Zero)) == LT))",fontsize=16,color="black",shape="box"];11 -> 15[label="",style="solid", color="black", weight=3];
12[label="prPr0 vuz3 (Pos Zero) (not (primCmpInt (Pos Zero) (fromInt (Pos Zero)) == LT))",fontsize=16,color="black",shape="box"];12 -> 16[label="",style="solid", color="black", weight=3];
13[label="prPr0 vuz3 (Neg (Succ vuz400)) (not (primCmpInt (Neg (Succ vuz400)) (fromInt (Pos Zero)) == LT))",fontsize=16,color="black",shape="box"];13 -> 17[label="",style="solid", color="black", weight=3];
14[label="prPr0 vuz3 (Neg Zero) (not (primCmpInt (Neg Zero) (fromInt (Pos Zero)) == LT))",fontsize=16,color="black",shape="box"];14 -> 18[label="",style="solid", color="black", weight=3];
15[label="prPr0 vuz3 (Pos (Succ vuz400)) (not (primCmpInt (Pos (Succ vuz400)) (Pos Zero) == LT))",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="prPr0 vuz3 (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == LT))",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="prPr0 vuz3 (Neg (Succ vuz400)) (not (primCmpInt (Neg (Succ vuz400)) (Pos Zero) == LT))",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="prPr0 vuz3 (Neg Zero) (not (primCmpInt (Neg Zero) (Pos Zero) == LT))",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="prPr0 vuz3 (Pos (Succ vuz400)) (not (primCmpNat (Succ vuz400) Zero == LT))",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="prPr0 vuz3 (Pos Zero) (not (EQ == LT))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="prPr0 vuz3 (Neg (Succ vuz400)) (not (LT == LT))",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="prPr0 vuz3 (Neg Zero) (not (EQ == LT))",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="prPr0 vuz3 (Pos (Succ vuz400)) (not (GT == LT))",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24[label="prPr0 vuz3 (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];24 -> 28[label="",style="solid", color="black", weight=3];
25[label="prPr0 vuz3 (Neg (Succ vuz400)) (not True)",fontsize=16,color="black",shape="box"];25 -> 29[label="",style="solid", color="black", weight=3];
26[label="prPr0 vuz3 (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];26 -> 30[label="",style="solid", color="black", weight=3];
27[label="prPr0 vuz3 (Pos (Succ vuz400)) (not False)",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="prPr0 vuz3 (Pos Zero) True",fontsize=16,color="black",shape="box"];28 -> 32[label="",style="solid", color="black", weight=3];
29[label="prPr0 vuz3 (Neg (Succ vuz400)) False",fontsize=16,color="black",shape="box"];29 -> 33[label="",style="solid", color="black", weight=3];
30[label="prPr0 vuz3 (Neg Zero) True",fontsize=16,color="black",shape="box"];30 -> 34[label="",style="solid", color="black", weight=3];
31[label="prPr0 vuz3 (Pos (Succ vuz400)) True",fontsize=16,color="black",shape="box"];31 -> 35[label="",style="solid", color="black", weight=3];
32[label="vuz3 ^ Pos Zero",fontsize=16,color="black",shape="box"];32 -> 36[label="",style="solid", color="black", weight=3];
33[label="recip (vuz3 ^ (`negate` Neg (Succ vuz400)))",fontsize=16,color="black",shape="box"];33 -> 37[label="",style="solid", color="black", weight=3];
34[label="vuz3 ^ Neg Zero",fontsize=16,color="black",shape="box"];34 -> 38[label="",style="solid", color="black", weight=3];
35[label="vuz3 ^ Pos (Succ vuz400)",fontsize=16,color="black",shape="box"];35 -> 39[label="",style="solid", color="black", weight=3];
36[label="pr4 vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];36 -> 40[label="",style="solid", color="black", weight=3];
37[label="fromInt (Pos (Succ Zero)) / vuz3 ^ (`negate` Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];37 -> 41[label="",style="solid", color="black", weight=3];
38[label="pr4 vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];38 -> 42[label="",style="solid", color="black", weight=3];
39[label="pr4 vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];39 -> 43[label="",style="solid", color="black", weight=3];
40[label="pr3 (Pos Zero == fromInt (Pos Zero)) vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];40 -> 44[label="",style="solid", color="black", weight=3];
41[label="primDivFloat (fromInt (Pos (Succ Zero))) (vuz3 ^ (`negate` Neg (Succ vuz400)))",fontsize=16,color="black",shape="box"];41 -> 45[label="",style="solid", color="black", weight=3];
42[label="pr3 (Neg Zero == fromInt (Pos Zero)) vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];42 -> 46[label="",style="solid", color="black", weight=3];
43[label="pr3 (Pos (Succ vuz400) == fromInt (Pos Zero)) vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];43 -> 47[label="",style="solid", color="black", weight=3];
44[label="pr3 (primEqInt (Pos Zero) (fromInt (Pos Zero))) vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];44 -> 48[label="",style="solid", color="black", weight=3];
45[label="primDivFloat (primIntToFloat (Pos (Succ Zero))) (vuz3 ^ (`negate` Neg (Succ vuz400)))",fontsize=16,color="black",shape="box"];45 -> 49[label="",style="solid", color="black", weight=3];
46[label="pr3 (primEqInt (Neg Zero) (fromInt (Pos Zero))) vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];46 -> 50[label="",style="solid", color="black", weight=3];
47[label="pr3 (primEqInt (Pos (Succ vuz400)) (fromInt (Pos Zero))) vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="triangle"];47 -> 51[label="",style="solid", color="black", weight=3];
48[label="pr3 (primEqInt (Pos Zero) (Pos Zero)) vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];48 -> 52[label="",style="solid", color="black", weight=3];
49 -> 68[label="",style="dashed", color="red", weight=0];
49[label="primDivFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (vuz3 ^ (`negate` Neg (Succ vuz400)))",fontsize=16,color="magenta"];49 -> 69[label="",style="dashed", color="magenta", weight=3];
50[label="pr3 (primEqInt (Neg Zero) (Pos Zero)) vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];50 -> 54[label="",style="solid", color="black", weight=3];
51[label="pr3 (primEqInt (Pos (Succ vuz400)) (Pos Zero)) vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];51 -> 55[label="",style="solid", color="black", weight=3];
52[label="pr3 True vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];52 -> 56[label="",style="solid", color="black", weight=3];
69[label="vuz3 ^ (`negate` Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];69 -> 75[label="",style="solid", color="black", weight=3];
68[label="primDivFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) vuz5",fontsize=16,color="burlywood",shape="triangle"];2097[label="vuz5/Float vuz50 vuz51",fontsize=10,color="white",style="solid",shape="box"];68 -> 2097[label="",style="solid", color="burlywood", weight=9];
2097 -> 76[label="",style="solid", color="burlywood", weight=3];
54[label="pr3 True vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];54 -> 58[label="",style="solid", color="black", weight=3];
55[label="pr3 False vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];55 -> 59[label="",style="solid", color="black", weight=3];
56[label="fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];56 -> 60[label="",style="solid", color="black", weight=3];
75[label="pr4 vuz3 (`negate` Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];75 -> 78[label="",style="solid", color="black", weight=3];
76[label="primDivFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (Float vuz50 vuz51)",fontsize=16,color="black",shape="box"];76 -> 79[label="",style="solid", color="black", weight=3];
58 -> 56[label="",style="dashed", color="red", weight=0];
58[label="fromInt (Pos (Succ Zero))",fontsize=16,color="magenta"];59[label="pr2 vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];59 -> 62[label="",style="solid", color="black", weight=3];
60[label="primIntToFloat (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];60 -> 63[label="",style="solid", color="black", weight=3];
78[label="pr3 (`negate` Neg (Succ vuz400) == fromInt (Pos Zero)) vuz3 (`negate` Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];78 -> 81[label="",style="solid", color="black", weight=3];
79[label="Float (Pos (Succ Zero) * vuz51) (Pos (Succ Zero) * vuz50)",fontsize=16,color="green",shape="box"];79 -> 82[label="",style="dashed", color="green", weight=3];
79 -> 83[label="",style="dashed", color="green", weight=3];
62[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (Pos (Succ vuz400) > fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];62 -> 65[label="",style="solid", color="black", weight=3];
63[label="Float (Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];81[label="pr3 (primEqInt (`negate` Neg (Succ vuz400)) (fromInt (Pos Zero))) vuz3 (`negate` Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];81 -> 85[label="",style="solid", color="black", weight=3];
82 -> 878[label="",style="dashed", color="red", weight=0];
82[label="Pos (Succ Zero) * vuz51",fontsize=16,color="magenta"];82 -> 879[label="",style="dashed", color="magenta", weight=3];
82 -> 880[label="",style="dashed", color="magenta", weight=3];
83 -> 878[label="",style="dashed", color="red", weight=0];
83[label="Pos (Succ Zero) * vuz50",fontsize=16,color="magenta"];83 -> 881[label="",style="dashed", color="magenta", weight=3];
83 -> 882[label="",style="dashed", color="magenta", weight=3];
65[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (compare (Pos (Succ vuz400)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];65 -> 67[label="",style="solid", color="black", weight=3];
85[label="pr3 (primEqInt (primNegInt (Neg (Succ vuz400))) (fromInt (Pos Zero))) vuz3 (primNegInt (Neg (Succ vuz400)))",fontsize=16,color="black",shape="box"];85 -> 89[label="",style="solid", color="black", weight=3];
879[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];880[label="vuz51",fontsize=16,color="green",shape="box"];878[label="vuz15 * vuz49",fontsize=16,color="black",shape="triangle"];878 -> 890[label="",style="solid", color="black", weight=3];
881[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];882[label="vuz50",fontsize=16,color="green",shape="box"];67[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (primCmpInt (Pos (Succ vuz400)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];67 -> 77[label="",style="solid", color="black", weight=3];
89 -> 47[label="",style="dashed", color="red", weight=0];
89[label="pr3 (primEqInt (Pos (Succ vuz400)) (fromInt (Pos Zero))) vuz3 (Pos (Succ vuz400))",fontsize=16,color="magenta"];89 -> 93[label="",style="dashed", color="magenta", weight=3];
890[label="primMulInt vuz15 vuz49",fontsize=16,color="burlywood",shape="box"];2102[label="vuz15/Pos vuz150",fontsize=10,color="white",style="solid",shape="box"];890 -> 2102[label="",style="solid", color="burlywood", weight=9];
2102 -> 903[label="",style="solid", color="burlywood", weight=3];
2103[label="vuz15/Neg vuz150",fontsize=10,color="white",style="solid",shape="box"];890 -> 2103[label="",style="solid", color="burlywood", weight=9];
2103 -> 904[label="",style="solid", color="burlywood", weight=3];
77[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (primCmpInt (Pos (Succ vuz400)) (Pos Zero) == GT)",fontsize=16,color="black",shape="box"];77 -> 80[label="",style="solid", color="black", weight=3];
93[label="vuz400",fontsize=16,color="green",shape="box"];903[label="primMulInt (Pos vuz150) vuz49",fontsize=16,color="burlywood",shape="box"];2104[label="vuz49/Pos vuz490",fontsize=10,color="white",style="solid",shape="box"];903 -> 2104[label="",style="solid", color="burlywood", weight=9];
2104 -> 917[label="",style="solid", color="burlywood", weight=3];
2105[label="vuz49/Neg vuz490",fontsize=10,color="white",style="solid",shape="box"];903 -> 2105[label="",style="solid", color="burlywood", weight=9];
2105 -> 918[label="",style="solid", color="burlywood", weight=3];
904[label="primMulInt (Neg vuz150) vuz49",fontsize=16,color="burlywood",shape="box"];2106[label="vuz49/Pos vuz490",fontsize=10,color="white",style="solid",shape="box"];904 -> 2106[label="",style="solid", color="burlywood", weight=9];
2106 -> 919[label="",style="solid", color="burlywood", weight=3];
2107[label="vuz49/Neg vuz490",fontsize=10,color="white",style="solid",shape="box"];904 -> 2107[label="",style="solid", color="burlywood", weight=9];
2107 -> 920[label="",style="solid", color="burlywood", weight=3];
80[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (primCmpNat (Succ vuz400) Zero == GT)",fontsize=16,color="black",shape="box"];80 -> 84[label="",style="solid", color="black", weight=3];
917[label="primMulInt (Pos vuz150) (Pos vuz490)",fontsize=16,color="black",shape="box"];917 -> 934[label="",style="solid", color="black", weight=3];
918[label="primMulInt (Pos vuz150) (Neg vuz490)",fontsize=16,color="black",shape="box"];918 -> 935[label="",style="solid", color="black", weight=3];
919[label="primMulInt (Neg vuz150) (Pos vuz490)",fontsize=16,color="black",shape="box"];919 -> 936[label="",style="solid", color="black", weight=3];
920[label="primMulInt (Neg vuz150) (Neg vuz490)",fontsize=16,color="black",shape="box"];920 -> 937[label="",style="solid", color="black", weight=3];
84[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (GT == GT)",fontsize=16,color="black",shape="box"];84 -> 88[label="",style="solid", color="black", weight=3];
934[label="Pos (primMulNat vuz150 vuz490)",fontsize=16,color="green",shape="box"];934 -> 948[label="",style="dashed", color="green", weight=3];
935[label="Neg (primMulNat vuz150 vuz490)",fontsize=16,color="green",shape="box"];935 -> 949[label="",style="dashed", color="green", weight=3];
936[label="Neg (primMulNat vuz150 vuz490)",fontsize=16,color="green",shape="box"];936 -> 950[label="",style="dashed", color="green", weight=3];
937[label="Pos (primMulNat vuz150 vuz490)",fontsize=16,color="green",shape="box"];937 -> 951[label="",style="dashed", color="green", weight=3];
88[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) True",fontsize=16,color="black",shape="box"];88 -> 92[label="",style="solid", color="black", weight=3];
948[label="primMulNat vuz150 vuz490",fontsize=16,color="burlywood",shape="triangle"];2108[label="vuz150/Succ vuz1500",fontsize=10,color="white",style="solid",shape="box"];948 -> 2108[label="",style="solid", color="burlywood", weight=9];
2108 -> 977[label="",style="solid", color="burlywood", weight=3];
2109[label="vuz150/Zero",fontsize=10,color="white",style="solid",shape="box"];948 -> 2109[label="",style="solid", color="burlywood", weight=9];
2109 -> 978[label="",style="solid", color="burlywood", weight=3];
949 -> 948[label="",style="dashed", color="red", weight=0];
949[label="primMulNat vuz150 vuz490",fontsize=16,color="magenta"];949 -> 979[label="",style="dashed", color="magenta", weight=3];
950 -> 948[label="",style="dashed", color="red", weight=0];
950[label="primMulNat vuz150 vuz490",fontsize=16,color="magenta"];950 -> 980[label="",style="dashed", color="magenta", weight=3];
951 -> 948[label="",style="dashed", color="red", weight=0];
951[label="primMulNat vuz150 vuz490",fontsize=16,color="magenta"];951 -> 981[label="",style="dashed", color="magenta", weight=3];
951 -> 982[label="",style="dashed", color="magenta", weight=3];
92[label="pr2F vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];92 -> 96[label="",style="solid", color="black", weight=3];
977[label="primMulNat (Succ vuz1500) vuz490",fontsize=16,color="burlywood",shape="box"];2113[label="vuz490/Succ vuz4900",fontsize=10,color="white",style="solid",shape="box"];977 -> 2113[label="",style="solid", color="burlywood", weight=9];
2113 -> 1019[label="",style="solid", color="burlywood", weight=3];
2114[label="vuz490/Zero",fontsize=10,color="white",style="solid",shape="box"];977 -> 2114[label="",style="solid", color="burlywood", weight=9];
2114 -> 1020[label="",style="solid", color="burlywood", weight=3];
978[label="primMulNat Zero vuz490",fontsize=16,color="burlywood",shape="box"];2115[label="vuz490/Succ vuz4900",fontsize=10,color="white",style="solid",shape="box"];978 -> 2115[label="",style="solid", color="burlywood", weight=9];
2115 -> 1021[label="",style="solid", color="burlywood", weight=3];
2116[label="vuz490/Zero",fontsize=10,color="white",style="solid",shape="box"];978 -> 2116[label="",style="solid", color="burlywood", weight=9];
2116 -> 1022[label="",style="solid", color="burlywood", weight=3];
979[label="vuz490",fontsize=16,color="green",shape="box"];980[label="vuz150",fontsize=16,color="green",shape="box"];981[label="vuz490",fontsize=16,color="green",shape="box"];982[label="vuz150",fontsize=16,color="green",shape="box"];96[label="pr2F4 vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];96 -> 99[label="",style="solid", color="black", weight=3];
1019[label="primMulNat (Succ vuz1500) (Succ vuz4900)",fontsize=16,color="black",shape="box"];1019 -> 1034[label="",style="solid", color="black", weight=3];
1020[label="primMulNat (Succ vuz1500) Zero",fontsize=16,color="black",shape="box"];1020 -> 1035[label="",style="solid", color="black", weight=3];
1021[label="primMulNat Zero (Succ vuz4900)",fontsize=16,color="black",shape="box"];1021 -> 1036[label="",style="solid", color="black", weight=3];
1022[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];1022 -> 1037[label="",style="solid", color="black", weight=3];
99[label="pr2F3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];99 -> 103[label="",style="solid", color="black", weight=3];
1034 -> 1045[label="",style="dashed", color="red", weight=0];
1034[label="primPlusNat (primMulNat vuz1500 (Succ vuz4900)) (Succ vuz4900)",fontsize=16,color="magenta"];1034 -> 1046[label="",style="dashed", color="magenta", weight=3];
1035[label="Zero",fontsize=16,color="green",shape="box"];1036[label="Zero",fontsize=16,color="green",shape="box"];1037[label="Zero",fontsize=16,color="green",shape="box"];103[label="pr2F3 (primEqInt (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];103 -> 106[label="",style="solid", color="black", weight=3];
1046 -> 948[label="",style="dashed", color="red", weight=0];
1046[label="primMulNat vuz1500 (Succ vuz4900)",fontsize=16,color="magenta"];1046 -> 1047[label="",style="dashed", color="magenta", weight=3];
1046 -> 1048[label="",style="dashed", color="magenta", weight=3];
1045[label="primPlusNat vuz58 (Succ vuz4900)",fontsize=16,color="burlywood",shape="triangle"];2119[label="vuz58/Succ vuz580",fontsize=10,color="white",style="solid",shape="box"];1045 -> 2119[label="",style="solid", color="burlywood", weight=9];
2119 -> 1049[label="",style="solid", color="burlywood", weight=3];
2120[label="vuz58/Zero",fontsize=10,color="white",style="solid",shape="box"];1045 -> 2120[label="",style="solid", color="burlywood", weight=9];
2120 -> 1050[label="",style="solid", color="burlywood", weight=3];
106[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz400)) (fromInt (Pos (Succ Zero)))) (fromInt (Pos Zero))) vuz3 (primMinusInt (Pos (Succ vuz400)) (fromInt (Pos (Succ Zero)))) vuz3",fontsize=16,color="black",shape="box"];106 -> 108[label="",style="solid", color="black", weight=3];
1047[label="Succ vuz4900",fontsize=16,color="green",shape="box"];1048[label="vuz1500",fontsize=16,color="green",shape="box"];1049[label="primPlusNat (Succ vuz580) (Succ vuz4900)",fontsize=16,color="black",shape="box"];1049 -> 1055[label="",style="solid", color="black", weight=3];
1050[label="primPlusNat Zero (Succ vuz4900)",fontsize=16,color="black",shape="box"];1050 -> 1056[label="",style="solid", color="black", weight=3];
108[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz400)) (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz3 (primMinusInt (Pos (Succ vuz400)) (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];108 -> 110[label="",style="solid", color="black", weight=3];
1055[label="Succ (Succ (primPlusNat vuz580 vuz4900))",fontsize=16,color="green",shape="box"];1055 -> 1061[label="",style="dashed", color="green", weight=3];
1056[label="Succ vuz4900",fontsize=16,color="green",shape="box"];110[label="pr2F3 (primEqInt (primMinusNat (Succ vuz400) (Succ Zero)) (fromInt (Pos Zero))) vuz3 (primMinusNat (Succ vuz400) (Succ Zero)) vuz3",fontsize=16,color="black",shape="box"];110 -> 111[label="",style="solid", color="black", weight=3];
1061[label="primPlusNat vuz580 vuz4900",fontsize=16,color="burlywood",shape="triangle"];2121[label="vuz580/Succ vuz5800",fontsize=10,color="white",style="solid",shape="box"];1061 -> 2121[label="",style="solid", color="burlywood", weight=9];
2121 -> 1068[label="",style="solid", color="burlywood", weight=3];
2122[label="vuz580/Zero",fontsize=10,color="white",style="solid",shape="box"];1061 -> 2122[label="",style="solid", color="burlywood", weight=9];
2122 -> 1069[label="",style="solid", color="burlywood", weight=3];
111[label="pr2F3 (primEqInt (primMinusNat vuz400 Zero) (fromInt (Pos Zero))) vuz3 (primMinusNat vuz400 Zero) vuz3",fontsize=16,color="burlywood",shape="box"];2123[label="vuz400/Succ vuz4000",fontsize=10,color="white",style="solid",shape="box"];111 -> 2123[label="",style="solid", color="burlywood", weight=9];
2123 -> 112[label="",style="solid", color="burlywood", weight=3];
2124[label="vuz400/Zero",fontsize=10,color="white",style="solid",shape="box"];111 -> 2124[label="",style="solid", color="burlywood", weight=9];
2124 -> 113[label="",style="solid", color="burlywood", weight=3];
1068[label="primPlusNat (Succ vuz5800) vuz4900",fontsize=16,color="burlywood",shape="box"];2125[label="vuz4900/Succ vuz49000",fontsize=10,color="white",style="solid",shape="box"];1068 -> 2125[label="",style="solid", color="burlywood", weight=9];
2125 -> 1077[label="",style="solid", color="burlywood", weight=3];
2126[label="vuz4900/Zero",fontsize=10,color="white",style="solid",shape="box"];1068 -> 2126[label="",style="solid", color="burlywood", weight=9];
2126 -> 1078[label="",style="solid", color="burlywood", weight=3];
1069[label="primPlusNat Zero vuz4900",fontsize=16,color="burlywood",shape="box"];2127[label="vuz4900/Succ vuz49000",fontsize=10,color="white",style="solid",shape="box"];1069 -> 2127[label="",style="solid", color="burlywood", weight=9];
2127 -> 1079[label="",style="solid", color="burlywood", weight=3];
2128[label="vuz4900/Zero",fontsize=10,color="white",style="solid",shape="box"];1069 -> 2128[label="",style="solid", color="burlywood", weight=9];
2128 -> 1080[label="",style="solid", color="burlywood", weight=3];
112[label="pr2F3 (primEqInt (primMinusNat (Succ vuz4000) Zero) (fromInt (Pos Zero))) vuz3 (primMinusNat (Succ vuz4000) Zero) vuz3",fontsize=16,color="black",shape="box"];112 -> 114[label="",style="solid", color="black", weight=3];
113[label="pr2F3 (primEqInt (primMinusNat Zero Zero) (fromInt (Pos Zero))) vuz3 (primMinusNat Zero Zero) vuz3",fontsize=16,color="black",shape="box"];113 -> 115[label="",style="solid", color="black", weight=3];
1077[label="primPlusNat (Succ vuz5800) (Succ vuz49000)",fontsize=16,color="black",shape="box"];1077 -> 1089[label="",style="solid", color="black", weight=3];
1078[label="primPlusNat (Succ vuz5800) Zero",fontsize=16,color="black",shape="box"];1078 -> 1090[label="",style="solid", color="black", weight=3];
1079[label="primPlusNat Zero (Succ vuz49000)",fontsize=16,color="black",shape="box"];1079 -> 1091[label="",style="solid", color="black", weight=3];
1080[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];1080 -> 1092[label="",style="solid", color="black", weight=3];
114[label="pr2F3 (primEqInt (Pos (Succ vuz4000)) (fromInt (Pos Zero))) vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];114 -> 116[label="",style="solid", color="black", weight=3];
115[label="pr2F3 (primEqInt (Pos Zero) (fromInt (Pos Zero))) vuz3 (Pos Zero) vuz3",fontsize=16,color="black",shape="box"];115 -> 117[label="",style="solid", color="black", weight=3];
1089[label="Succ (Succ (primPlusNat vuz5800 vuz49000))",fontsize=16,color="green",shape="box"];1089 -> 1101[label="",style="dashed", color="green", weight=3];
1090[label="Succ vuz5800",fontsize=16,color="green",shape="box"];1091[label="Succ vuz49000",fontsize=16,color="green",shape="box"];1092[label="Zero",fontsize=16,color="green",shape="box"];116[label="pr2F3 (primEqInt (Pos (Succ vuz4000)) (Pos Zero)) vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];116 -> 118[label="",style="solid", color="black", weight=3];
117[label="pr2F3 (primEqInt (Pos Zero) (Pos Zero)) vuz3 (Pos Zero) vuz3",fontsize=16,color="black",shape="box"];117 -> 119[label="",style="solid", color="black", weight=3];
1101 -> 1061[label="",style="dashed", color="red", weight=0];
1101[label="primPlusNat vuz5800 vuz49000",fontsize=16,color="magenta"];1101 -> 1111[label="",style="dashed", color="magenta", weight=3];
1101 -> 1112[label="",style="dashed", color="magenta", weight=3];
118[label="pr2F3 False vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];118 -> 120[label="",style="solid", color="black", weight=3];
119[label="pr2F3 True vuz3 (Pos Zero) vuz3",fontsize=16,color="black",shape="box"];119 -> 121[label="",style="solid", color="black", weight=3];
1111[label="vuz5800",fontsize=16,color="green",shape="box"];1112[label="vuz49000",fontsize=16,color="green",shape="box"];120[label="pr2F0 vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];120 -> 122[label="",style="solid", color="black", weight=3];
121[label="vuz3",fontsize=16,color="green",shape="box"];122[label="pr2F0G vuz3 vuz3 (Pos (Succ vuz4000))",fontsize=16,color="black",shape="box"];122 -> 123[label="",style="solid", color="black", weight=3];
123[label="pr2F0G2 vuz3 vuz3 (Pos (Succ vuz4000))",fontsize=16,color="black",shape="box"];123 -> 124[label="",style="solid", color="black", weight=3];
124[label="pr2F0G1 vuz3 vuz3 (Pos (Succ vuz4000)) (even (Pos (Succ vuz4000)))",fontsize=16,color="black",shape="box"];124 -> 125[label="",style="solid", color="black", weight=3];
125[label="pr2F0G1 vuz3 vuz3 (Pos (Succ vuz4000)) (primEvenInt (Pos (Succ vuz4000)))",fontsize=16,color="black",shape="box"];125 -> 126[label="",style="solid", color="black", weight=3];
126 -> 159[label="",style="dashed", color="red", weight=0];
126[label="pr2F0G1 vuz3 vuz3 (Pos (Succ vuz4000)) (primEvenNat (Succ vuz4000))",fontsize=16,color="magenta"];126 -> 160[label="",style="dashed", color="magenta", weight=3];
126 -> 161[label="",style="dashed", color="magenta", weight=3];
126 -> 162[label="",style="dashed", color="magenta", weight=3];
160[label="vuz4000",fontsize=16,color="green",shape="box"];161[label="Succ vuz4000",fontsize=16,color="green",shape="box"];162[label="vuz3",fontsize=16,color="green",shape="box"];159[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) (primEvenNat vuz9)\n  Num a",fontsize=16,color="burlywood",shape="triangle"];2131[label="vuz9/Succ vuz90",fontsize=10,color="white",style="solid",shape="box"];159 -> 2131[label="",style="solid", color="burlywood", weight=9];
2131 -> 172[label="",style="solid", color="burlywood", weight=3];
2132[label="vuz9/Zero",fontsize=10,color="white",style="solid",shape="box"];159 -> 2132[label="",style="solid", color="burlywood", weight=9];
2132 -> 173[label="",style="solid", color="burlywood", weight=3];
172[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) (primEvenNat (Succ vuz90))\n  Num a",fontsize=16,color="burlywood",shape="box"];2133[label="vuz90/Succ vuz900",fontsize=10,color="white",style="solid",shape="box"];172 -> 2133[label="",style="solid", color="burlywood", weight=9];
2133 -> 174[label="",style="solid", color="burlywood", weight=3];
2134[label="vuz90/Zero",fontsize=10,color="white",style="solid",shape="box"];172 -> 2134[label="",style="solid", color="burlywood", weight=9];
2134 -> 175[label="",style="solid", color="burlywood", weight=3];
173[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="box"];173 -> 176[label="",style="solid", color="black", weight=3];
174[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) (primEvenNat (Succ (Succ vuz900)))\n  Num a",fontsize=16,color="black",shape="box"];174 -> 177[label="",style="solid", color="black", weight=3];
175[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) (primEvenNat (Succ Zero))\n  Num a",fontsize=16,color="black",shape="box"];175 -> 178[label="",style="solid", color="black", weight=3];
176[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) True\n  Num a",fontsize=16,color="black",shape="box"];176 -> 179[label="",style="solid", color="black", weight=3];
177 -> 159[label="",style="dashed", color="red", weight=0];
177[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) (primEvenNat vuz900)\n  Num a",fontsize=16,color="magenta"];177 -> 180[label="",style="dashed", color="magenta", weight=3];
178[label="pr2F0G1 vuz7 vuz7 (Pos (Succ vuz8)) False\n  Num a",fontsize=16,color="black",shape="box"];178 -> 181[label="",style="solid", color="black", weight=3];
179[label="pr2F0G vuz7 (vuz7 * vuz7) (Pos (Succ vuz8) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];179 -> 182[label="",style="solid", color="black", weight=3];
180[label="vuz900",fontsize=16,color="green",shape="box"];181[label="pr2F0G0 vuz7 vuz7 (Pos (Succ vuz8)) otherwise\n  Num a",fontsize=16,color="black",shape="box"];181 -> 183[label="",style="solid", color="black", weight=3];
182[label="pr2F0G2 vuz7 (vuz7 * vuz7) (Pos (Succ vuz8) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];182 -> 184[label="",style="solid", color="black", weight=3];
183[label="pr2F0G0 vuz7 vuz7 (Pos (Succ vuz8)) True\n  Num a",fontsize=16,color="black",shape="box"];183 -> 185[label="",style="solid", color="black", weight=3];
184[label="pr2F0G1 vuz7 (vuz7 * vuz7) (Pos (Succ vuz8) `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos (Succ vuz8) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];184 -> 186[label="",style="solid", color="black", weight=3];
185[label="pr2F vuz7 (Pos (Succ vuz8) - fromInt (Pos (Succ Zero))) (vuz7 * vuz7)\n  Num a",fontsize=16,color="black",shape="box"];185 -> 187[label="",style="solid", color="black", weight=3];
186[label="pr2F0G1 vuz7 (vuz7 * vuz7) (Pos (Succ vuz8) `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos (Succ vuz8) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];186 -> 188[label="",style="solid", color="black", weight=3];
187[label="pr2F4 vuz7 (Pos (Succ vuz8) - fromInt (Pos (Succ Zero))) (vuz7 * vuz7)\n  Num a",fontsize=16,color="black",shape="box"];187 -> 189[label="",style="solid", color="black", weight=3];
188[label="pr2F0G1 vuz7 (vuz7 * vuz7) (primQuotInt (Pos (Succ vuz8)) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos (Succ vuz8)) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="black",shape="box"];188 -> 190[label="",style="solid", color="black", weight=3];
189[label="pr2F3 (Pos (Succ vuz8) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) vuz7 (Pos (Succ vuz8) - fromInt (Pos (Succ Zero))) (vuz7 * vuz7)\n  Num a",fontsize=16,color="black",shape="box"];189 -> 191[label="",style="solid", color="black", weight=3];
190 -> 997[label="",style="dashed", color="red", weight=0];
190[label="pr2F0G1 vuz7 (vuz7 * vuz7) (primQuotInt (Pos (Succ vuz8)) (Pos (Succ (Succ Zero)))) (primEvenInt (primQuotInt (Pos (Succ vuz8)) (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];190 -> 998[label="",style="dashed", color="magenta", weight=3];
190 -> 999[label="",style="dashed", color="magenta", weight=3];
190 -> 1000[label="",style="dashed", color="magenta", weight=3];
191 -> 1919[label="",style="dashed", color="red", weight=0];
191[label="pr2F3 (primEqInt (Pos (Succ vuz8) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz7 (Pos (Succ vuz8) - fromInt (Pos (Succ Zero))) (vuz7 * vuz7)\n  Num a",fontsize=16,color="magenta"];191 -> 1920[label="",style="dashed", color="magenta", weight=3];
191 -> 1921[label="",style="dashed", color="magenta", weight=3];
191 -> 1922[label="",style="dashed", color="magenta", weight=3];
998[label="vuz7\n  Num a",fontsize=16,color="green",shape="box"];999[label="vuz7\n  Num a",fontsize=16,color="green",shape="box"];1000[label="Succ vuz8",fontsize=16,color="green",shape="box"];997[label="pr2F0G1 vuz55 (vuz56 * vuz56) (primQuotInt (Pos vuz57) (Pos (Succ (Succ Zero)))) (primEvenInt (primQuotInt (Pos vuz57) (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="triangle"];997 -> 1023[label="",style="solid", color="black", weight=3];
1920[label="vuz7\n  Num a",fontsize=16,color="green",shape="box"];1921[label="vuz8",fontsize=16,color="green",shape="box"];1922[label="vuz7\n  Num a",fontsize=16,color="green",shape="box"];1919[label="pr2F3 (primEqInt (Pos (Succ vuz88) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz89 (Pos (Succ vuz88) - fromInt (Pos (Succ Zero))) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="triangle"];1919 -> 1941[label="",style="solid", color="black", weight=3];
1023[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS vuz57 (Succ (Succ Zero)))) (primEvenInt (Pos (primDivNatS vuz57 (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1023 -> 1038[label="",style="solid", color="black", weight=3];
1941[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz88)) (fromInt (Pos (Succ Zero)))) (fromInt (Pos Zero))) vuz89 (primMinusInt (Pos (Succ vuz88)) (fromInt (Pos (Succ Zero)))) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1941 -> 1947[label="",style="solid", color="black", weight=3];
1038[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS vuz57 (Succ (Succ Zero)))) (primEvenNat (primDivNatS vuz57 (Succ (Succ Zero))))\n  Num a",fontsize=16,color="burlywood",shape="box"];2138[label="vuz57/Succ vuz570",fontsize=10,color="white",style="solid",shape="box"];1038 -> 2138[label="",style="solid", color="burlywood", weight=9];
2138 -> 1051[label="",style="solid", color="burlywood", weight=3];
2139[label="vuz57/Zero",fontsize=10,color="white",style="solid",shape="box"];1038 -> 2139[label="",style="solid", color="burlywood", weight=9];
2139 -> 1052[label="",style="solid", color="burlywood", weight=3];
1947[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz88)) (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz89 (primMinusInt (Pos (Succ vuz88)) (Pos (Succ Zero))) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1947 -> 1953[label="",style="solid", color="black", weight=3];
1051[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS (Succ vuz570) (Succ (Succ Zero)))) (primEvenNat (primDivNatS (Succ vuz570) (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1051 -> 1057[label="",style="solid", color="black", weight=3];
1052[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS Zero (Succ (Succ Zero)))) (primEvenNat (primDivNatS Zero (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1052 -> 1058[label="",style="solid", color="black", weight=3];
1953[label="pr2F3 (primEqInt (primMinusNat (Succ vuz88) (Succ Zero)) (fromInt (Pos Zero))) vuz89 (primMinusNat (Succ vuz88) (Succ Zero)) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1953 -> 1954[label="",style="solid", color="black", weight=3];
1057[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 vuz570 (Succ Zero) (primGEqNatS vuz570 (Succ Zero)))) (primEvenNat (primDivNatS0 vuz570 (Succ Zero) (primGEqNatS vuz570 (Succ Zero))))\n  Num a",fontsize=16,color="burlywood",shape="box"];2140[label="vuz570/Succ vuz5700",fontsize=10,color="white",style="solid",shape="box"];1057 -> 2140[label="",style="solid", color="burlywood", weight=9];
2140 -> 1062[label="",style="solid", color="burlywood", weight=3];
2141[label="vuz570/Zero",fontsize=10,color="white",style="solid",shape="box"];1057 -> 2141[label="",style="solid", color="burlywood", weight=9];
2141 -> 1063[label="",style="solid", color="burlywood", weight=3];
1058[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos Zero) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="triangle"];1058 -> 1064[label="",style="solid", color="black", weight=3];
1954[label="pr2F3 (primEqInt (primMinusNat vuz88 Zero) (fromInt (Pos Zero))) vuz89 (primMinusNat vuz88 Zero) (vuz89 * vuz90)\n  Num a",fontsize=16,color="burlywood",shape="box"];2142[label="vuz88/Succ vuz880",fontsize=10,color="white",style="solid",shape="box"];1954 -> 2142[label="",style="solid", color="burlywood", weight=9];
2142 -> 1955[label="",style="solid", color="burlywood", weight=3];
2143[label="vuz88/Zero",fontsize=10,color="white",style="solid",shape="box"];1954 -> 2143[label="",style="solid", color="burlywood", weight=9];
2143 -> 1956[label="",style="solid", color="burlywood", weight=3];
1062[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 (Succ vuz5700) (Succ Zero) (primGEqNatS (Succ vuz5700) (Succ Zero)))) (primEvenNat (primDivNatS0 (Succ vuz5700) (Succ Zero) (primGEqNatS (Succ vuz5700) (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1062 -> 1070[label="",style="solid", color="black", weight=3];
1063[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 Zero (Succ Zero) (primGEqNatS Zero (Succ Zero)))) (primEvenNat (primDivNatS0 Zero (Succ Zero) (primGEqNatS Zero (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1063 -> 1071[label="",style="solid", color="black", weight=3];
1064[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos Zero) True\n  Num a",fontsize=16,color="black",shape="box"];1064 -> 1072[label="",style="solid", color="black", weight=3];
1955[label="pr2F3 (primEqInt (primMinusNat (Succ vuz880) Zero) (fromInt (Pos Zero))) vuz89 (primMinusNat (Succ vuz880) Zero) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1955 -> 1957[label="",style="solid", color="black", weight=3];
1956[label="pr2F3 (primEqInt (primMinusNat Zero Zero) (fromInt (Pos Zero))) vuz89 (primMinusNat Zero Zero) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1956 -> 1958[label="",style="solid", color="black", weight=3];
1070[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 (Succ vuz5700) (Succ Zero) (primGEqNatS vuz5700 Zero))) (primEvenNat (primDivNatS0 (Succ vuz5700) (Succ Zero) (primGEqNatS vuz5700 Zero)))\n  Num a",fontsize=16,color="burlywood",shape="box"];2144[label="vuz5700/Succ vuz57000",fontsize=10,color="white",style="solid",shape="box"];1070 -> 2144[label="",style="solid", color="burlywood", weight=9];
2144 -> 1081[label="",style="solid", color="burlywood", weight=3];
2145[label="vuz5700/Zero",fontsize=10,color="white",style="solid",shape="box"];1070 -> 2145[label="",style="solid", color="burlywood", weight=9];
2145 -> 1082[label="",style="solid", color="burlywood", weight=3];
1071[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 Zero (Succ Zero) False)) (primEvenNat (primDivNatS0 Zero (Succ Zero) False))\n  Num a",fontsize=16,color="black",shape="box"];1071 -> 1083[label="",style="solid", color="black", weight=3];
1072[label="pr2F0G vuz55 (vuz56 * vuz56 * (vuz56 * vuz56)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1072 -> 1084[label="",style="solid", color="black", weight=3];
1957[label="pr2F3 (primEqInt (Pos (Succ vuz880)) (fromInt (Pos Zero))) vuz89 (Pos (Succ vuz880)) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1957 -> 1959[label="",style="solid", color="black", weight=3];
1958[label="pr2F3 (primEqInt (Pos Zero) (fromInt (Pos Zero))) vuz89 (Pos Zero) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1958 -> 1960[label="",style="solid", color="black", weight=3];
1081[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 (Succ (Succ vuz57000)) (Succ Zero) (primGEqNatS (Succ vuz57000) Zero))) (primEvenNat (primDivNatS0 (Succ (Succ vuz57000)) (Succ Zero) (primGEqNatS (Succ vuz57000) Zero)))\n  Num a",fontsize=16,color="black",shape="box"];1081 -> 1093[label="",style="solid", color="black", weight=3];
1082[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 (Succ Zero) (Succ Zero) (primGEqNatS Zero Zero))) (primEvenNat (primDivNatS0 (Succ Zero) (Succ Zero) (primGEqNatS Zero Zero)))\n  Num a",fontsize=16,color="black",shape="box"];1082 -> 1094[label="",style="solid", color="black", weight=3];
1083 -> 1058[label="",style="dashed", color="red", weight=0];
1083[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos Zero) (primEvenNat Zero)\n  Num a",fontsize=16,color="magenta"];1084[label="pr2F0G2 vuz55 (vuz56 * vuz56 * (vuz56 * vuz56)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1084 -> 1095[label="",style="solid", color="black", weight=3];
1959[label="pr2F3 (primEqInt (Pos (Succ vuz880)) (Pos Zero)) vuz89 (Pos (Succ vuz880)) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1959 -> 1961[label="",style="solid", color="black", weight=3];
1960[label="pr2F3 (primEqInt (Pos Zero) (Pos Zero)) vuz89 (Pos Zero) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1960 -> 1962[label="",style="solid", color="black", weight=3];
1093[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 (Succ (Succ vuz57000)) (Succ Zero) True)) (primEvenNat (primDivNatS0 (Succ (Succ vuz57000)) (Succ Zero) True))\n  Num a",fontsize=16,color="black",shape="box"];1093 -> 1102[label="",style="solid", color="black", weight=3];
1094[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (primDivNatS0 (Succ Zero) (Succ Zero) True)) (primEvenNat (primDivNatS0 (Succ Zero) (Succ Zero) True))\n  Num a",fontsize=16,color="black",shape="box"];1094 -> 1103[label="",style="solid", color="black", weight=3];
1095[label="pr2F0G1 vuz55 (vuz56 * vuz56 * (vuz56 * vuz56)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1095 -> 1104[label="",style="solid", color="black", weight=3];
1961[label="pr2F3 False vuz89 (Pos (Succ vuz880)) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1961 -> 1963[label="",style="solid", color="black", weight=3];
1962[label="pr2F3 True vuz89 (Pos Zero) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1962 -> 1964[label="",style="solid", color="black", weight=3];
1102 -> 1315[label="",style="dashed", color="red", weight=0];
1102[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (Succ (primDivNatS (primMinusNatS (Succ (Succ vuz57000)) (Succ Zero)) (Succ (Succ Zero))))) (primEvenNat (Succ (primDivNatS (primMinusNatS (Succ (Succ vuz57000)) (Succ Zero)) (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];1102 -> 1316[label="",style="dashed", color="magenta", weight=3];
1102 -> 1317[label="",style="dashed", color="magenta", weight=3];
1102 -> 1318[label="",style="dashed", color="magenta", weight=3];
1102 -> 1319[label="",style="dashed", color="magenta", weight=3];
1103 -> 1315[label="",style="dashed", color="red", weight=0];
1103[label="pr2F0G1 vuz55 (vuz56 * vuz56) (Pos (Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))))) (primEvenNat (Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];1103 -> 1320[label="",style="dashed", color="magenta", weight=3];
1103 -> 1321[label="",style="dashed", color="magenta", weight=3];
1103 -> 1322[label="",style="dashed", color="magenta", weight=3];
1103 -> 1323[label="",style="dashed", color="magenta", weight=3];
1104[label="pr2F0G1 vuz55 (vuz56 * vuz56 * (vuz56 * vuz56)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1104 -> 1115[label="",style="solid", color="black", weight=3];
1963[label="pr2F0 vuz89 (Pos (Succ vuz880)) (vuz89 * vuz90)\n  Num a",fontsize=16,color="black",shape="box"];1963 -> 1965[label="",style="solid", color="black", weight=3];
1964[label="vuz89 * vuz90\n  Num a",fontsize=16,color="blue",shape="box"];2149[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1964 -> 2149[label="",style="solid", color="blue", weight=9];
2149 -> 1966[label="",style="solid", color="blue", weight=3];
2150[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1964 -> 2150[label="",style="solid", color="blue", weight=9];
2150 -> 1967[label="",style="solid", color="blue", weight=3];
2151[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1964 -> 2151[label="",style="solid", color="blue", weight=9];
2151 -> 1968[label="",style="solid", color="blue", weight=3];
2152[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1964 -> 2152[label="",style="solid", color="blue", weight=9];
2152 -> 1969[label="",style="solid", color="blue", weight=3];
2153[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1964 -> 2153[label="",style="solid", color="blue", weight=9];
2153 -> 1970[label="",style="solid", color="blue", weight=3];
1316[label="vuz56\n  Num a",fontsize=16,color="green",shape="box"];1317[label="Succ (primDivNatS (primMinusNatS (Succ (Succ vuz57000)) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1317 -> 1340[label="",style="dashed", color="green", weight=3];
1318[label="primDivNatS (primMinusNatS (Succ (Succ vuz57000)) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="black",shape="triangle"];1318 -> 1341[label="",style="solid", color="black", weight=3];
1319[label="vuz55\n  Num a",fontsize=16,color="green",shape="box"];1315[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) (primEvenNat vuz71)\n  Num a",fontsize=16,color="burlywood",shape="triangle"];2154[label="vuz71/Succ vuz710",fontsize=10,color="white",style="solid",shape="box"];1315 -> 2154[label="",style="solid", color="burlywood", weight=9];
2154 -> 1342[label="",style="solid", color="burlywood", weight=3];
2155[label="vuz71/Zero",fontsize=10,color="white",style="solid",shape="box"];1315 -> 2155[label="",style="solid", color="burlywood", weight=9];
2155 -> 1343[label="",style="solid", color="burlywood", weight=3];
1320[label="vuz56\n  Num a",fontsize=16,color="green",shape="box"];1321[label="Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1321 -> 1344[label="",style="dashed", color="green", weight=3];
1322[label="primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="black",shape="triangle"];1322 -> 1345[label="",style="solid", color="black", weight=3];
1323[label="vuz55\n  Num a",fontsize=16,color="green",shape="box"];1115[label="pr2F0G1 vuz55 (vuz56 * vuz56 * (vuz56 * vuz56)) (primQuotInt (Pos Zero) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos Zero) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="black",shape="box"];1115 -> 1124[label="",style="solid", color="black", weight=3];
1965[label="pr2F0G (vuz89 * vuz90) vuz89 (Pos (Succ vuz880))\n  Num a",fontsize=16,color="black",shape="box"];1965 -> 1971[label="",style="solid", color="black", weight=3];
1966 -> 878[label="",style="dashed", color="red", weight=0];
1966[label="vuz89 * vuz90",fontsize=16,color="magenta"];1966 -> 1972[label="",style="dashed", color="magenta", weight=3];
1966 -> 1973[label="",style="dashed", color="magenta", weight=3];
1967 -> 899[label="",style="dashed", color="red", weight=0];
1967[label="vuz89 * vuz90",fontsize=16,color="magenta"];1967 -> 1974[label="",style="dashed", color="magenta", weight=3];
1967 -> 1975[label="",style="dashed", color="magenta", weight=3];
1968 -> 913[label="",style="dashed", color="red", weight=0];
1968[label="vuz89 * vuz90",fontsize=16,color="magenta"];1968 -> 1976[label="",style="dashed", color="magenta", weight=3];
1968 -> 1977[label="",style="dashed", color="magenta", weight=3];
1969 -> 930[label="",style="dashed", color="red", weight=0];
1969[label="vuz89 * vuz90\n  Integral a",fontsize=16,color="magenta"];1969 -> 1978[label="",style="dashed", color="magenta", weight=3];
1969 -> 1979[label="",style="dashed", color="magenta", weight=3];
1970 -> 944[label="",style="dashed", color="red", weight=0];
1970[label="vuz89 * vuz90",fontsize=16,color="magenta"];1970 -> 1980[label="",style="dashed", color="magenta", weight=3];
1970 -> 1981[label="",style="dashed", color="magenta", weight=3];
1340 -> 1318[label="",style="dashed", color="red", weight=0];
1340[label="primDivNatS (primMinusNatS (Succ (Succ vuz57000)) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1341[label="primDivNatS (primMinusNatS (Succ vuz57000) Zero) (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1341 -> 1348[label="",style="solid", color="black", weight=3];
1342[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) (primEvenNat (Succ vuz710))\n  Num a",fontsize=16,color="burlywood",shape="box"];2162[label="vuz710/Succ vuz7100",fontsize=10,color="white",style="solid",shape="box"];1342 -> 2162[label="",style="solid", color="burlywood", weight=9];
2162 -> 1349[label="",style="solid", color="burlywood", weight=3];
2163[label="vuz710/Zero",fontsize=10,color="white",style="solid",shape="box"];1342 -> 2163[label="",style="solid", color="burlywood", weight=9];
2163 -> 1350[label="",style="solid", color="burlywood", weight=3];
1343[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="box"];1343 -> 1351[label="",style="solid", color="black", weight=3];
1344 -> 1322[label="",style="dashed", color="red", weight=0];
1344[label="primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1345[label="primDivNatS (primMinusNatS Zero Zero) (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1345 -> 1352[label="",style="solid", color="black", weight=3];
1124 -> 997[label="",style="dashed", color="red", weight=0];
1124[label="pr2F0G1 vuz55 (vuz56 * vuz56 * (vuz56 * vuz56)) (primQuotInt (Pos Zero) (Pos (Succ (Succ Zero)))) (primEvenInt (primQuotInt (Pos Zero) (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];1124 -> 1140[label="",style="dashed", color="magenta", weight=3];
1124 -> 1141[label="",style="dashed", color="magenta", weight=3];
1971[label="pr2F0G2 (vuz89 * vuz90) vuz89 (Pos (Succ vuz880))\n  Num a",fontsize=16,color="black",shape="box"];1971 -> 1982[label="",style="solid", color="black", weight=3];
1972[label="vuz89",fontsize=16,color="green",shape="box"];1973[label="vuz90",fontsize=16,color="green",shape="box"];1974[label="vuz89",fontsize=16,color="green",shape="box"];1975[label="vuz90",fontsize=16,color="green",shape="box"];899[label="vuz15 * vuz50",fontsize=16,color="black",shape="triangle"];899 -> 905[label="",style="solid", color="black", weight=3];
1976[label="vuz90",fontsize=16,color="green",shape="box"];1977[label="vuz89",fontsize=16,color="green",shape="box"];913[label="vuz15 * vuz51",fontsize=16,color="black",shape="triangle"];913 -> 921[label="",style="solid", color="black", weight=3];
1978[label="vuz90\n  Integral a",fontsize=16,color="green",shape="box"];1979[label="vuz89\n  Integral a",fontsize=16,color="green",shape="box"];930[label="vuz15 * vuz52\n  Integral a",fontsize=16,color="black",shape="triangle"];930 -> 938[label="",style="solid", color="black", weight=3];
1980[label="vuz89",fontsize=16,color="green",shape="box"];1981[label="vuz90",fontsize=16,color="green",shape="box"];944[label="vuz15 * vuz53",fontsize=16,color="black",shape="triangle"];944 -> 952[label="",style="solid", color="black", weight=3];
1348[label="primDivNatS (Succ vuz57000) (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1348 -> 1355[label="",style="solid", color="black", weight=3];
1349[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) (primEvenNat (Succ (Succ vuz7100)))\n  Num a",fontsize=16,color="black",shape="box"];1349 -> 1356[label="",style="solid", color="black", weight=3];
1350[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) (primEvenNat (Succ Zero))\n  Num a",fontsize=16,color="black",shape="box"];1350 -> 1357[label="",style="solid", color="black", weight=3];
1351[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) True\n  Num a",fontsize=16,color="black",shape="box"];1351 -> 1358[label="",style="solid", color="black", weight=3];
1352[label="primDivNatS Zero (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1352 -> 1359[label="",style="solid", color="black", weight=3];
1140[label="vuz56 * vuz56\n  Num a",fontsize=16,color="blue",shape="box"];2166[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1140 -> 2166[label="",style="solid", color="blue", weight=9];
2166 -> 1147[label="",style="solid", color="blue", weight=3];
2167[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1140 -> 2167[label="",style="solid", color="blue", weight=9];
2167 -> 1148[label="",style="solid", color="blue", weight=3];
2168[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1140 -> 2168[label="",style="solid", color="blue", weight=9];
2168 -> 1149[label="",style="solid", color="blue", weight=3];
2169[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1140 -> 2169[label="",style="solid", color="blue", weight=9];
2169 -> 1150[label="",style="solid", color="blue", weight=3];
2170[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1140 -> 2170[label="",style="solid", color="blue", weight=9];
2170 -> 1151[label="",style="solid", color="blue", weight=3];
1141[label="Zero",fontsize=16,color="green",shape="box"];1982[label="pr2F0G1 (vuz89 * vuz90) vuz89 (Pos (Succ vuz880)) (even (Pos (Succ vuz880)))\n  Num a",fontsize=16,color="black",shape="box"];1982 -> 1983[label="",style="solid", color="black", weight=3];
905[label="primMulFloat vuz15 vuz50",fontsize=16,color="burlywood",shape="box"];2171[label="vuz15/Float vuz150 vuz151",fontsize=10,color="white",style="solid",shape="box"];905 -> 2171[label="",style="solid", color="burlywood", weight=9];
2171 -> 922[label="",style="solid", color="burlywood", weight=3];
921[label="error []",fontsize=16,color="red",shape="box"];938[label="error []",fontsize=16,color="red",shape="box"];952[label="error []",fontsize=16,color="red",shape="box"];1355[label="primDivNatS0 vuz57000 (Succ Zero) (primGEqNatS vuz57000 (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2172[label="vuz57000/Succ vuz570000",fontsize=10,color="white",style="solid",shape="box"];1355 -> 2172[label="",style="solid", color="burlywood", weight=9];
2172 -> 1362[label="",style="solid", color="burlywood", weight=3];
2173[label="vuz57000/Zero",fontsize=10,color="white",style="solid",shape="box"];1355 -> 2173[label="",style="solid", color="burlywood", weight=9];
2173 -> 1363[label="",style="solid", color="burlywood", weight=3];
1356 -> 1315[label="",style="dashed", color="red", weight=0];
1356[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) (primEvenNat vuz7100)\n  Num a",fontsize=16,color="magenta"];1356 -> 1364[label="",style="dashed", color="magenta", weight=3];
1357[label="pr2F0G1 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) False\n  Num a",fontsize=16,color="black",shape="box"];1357 -> 1365[label="",style="solid", color="black", weight=3];
1358[label="pr2F0G vuz68 (vuz69 * vuz69 * (vuz69 * vuz69)) (Pos (Succ vuz70) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1358 -> 1366[label="",style="solid", color="black", weight=3];
1359[label="Zero",fontsize=16,color="green",shape="box"];1147 -> 229[label="",style="dashed", color="red", weight=0];
1147[label="vuz56 * vuz56",fontsize=16,color="magenta"];1147 -> 1158[label="",style="dashed", color="magenta", weight=3];
1148 -> 230[label="",style="dashed", color="red", weight=0];
1148[label="vuz56 * vuz56",fontsize=16,color="magenta"];1148 -> 1159[label="",style="dashed", color="magenta", weight=3];
1149 -> 231[label="",style="dashed", color="red", weight=0];
1149[label="vuz56 * vuz56",fontsize=16,color="magenta"];1149 -> 1160[label="",style="dashed", color="magenta", weight=3];
1150 -> 232[label="",style="dashed", color="red", weight=0];
1150[label="vuz56 * vuz56\n  Integral a",fontsize=16,color="magenta"];1150 -> 1161[label="",style="dashed", color="magenta", weight=3];
1151 -> 233[label="",style="dashed", color="red", weight=0];
1151[label="vuz56 * vuz56",fontsize=16,color="magenta"];1151 -> 1162[label="",style="dashed", color="magenta", weight=3];
1983[label="pr2F0G1 (vuz89 * vuz90) vuz89 (Pos (Succ vuz880)) (primEvenInt (Pos (Succ vuz880)))\n  Num a",fontsize=16,color="black",shape="box"];1983 -> 1984[label="",style="solid", color="black", weight=3];
922[label="primMulFloat (Float vuz150 vuz151) vuz50",fontsize=16,color="burlywood",shape="box"];2180[label="vuz50/Float vuz500 vuz501",fontsize=10,color="white",style="solid",shape="box"];922 -> 2180[label="",style="solid", color="burlywood", weight=9];
2180 -> 939[label="",style="solid", color="burlywood", weight=3];
1362[label="primDivNatS0 (Succ vuz570000) (Succ Zero) (primGEqNatS (Succ vuz570000) (Succ Zero))",fontsize=16,color="black",shape="box"];1362 -> 1369[label="",style="solid", color="black", weight=3];
1363[label="primDivNatS0 Zero (Succ Zero) (primGEqNatS Zero (Succ Zero))",fontsize=16,color="black",shape="box"];1363 -> 1370[label="",style="solid", color="black", weight=3];
1364[label="vuz7100",fontsize=16,color="green",shape="box"];1365[label="pr2F0G0 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) otherwise\n  Num a",fontsize=16,color="black",shape="box"];1365 -> 1371[label="",style="solid", color="black", weight=3];
1366[label="pr2F0G2 vuz68 (vuz69 * vuz69 * (vuz69 * vuz69)) (Pos (Succ vuz70) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1366 -> 1372[label="",style="solid", color="black", weight=3];
1158[label="vuz56",fontsize=16,color="green",shape="box"];229 -> 878[label="",style="dashed", color="red", weight=0];
229[label="vuz7 * vuz7",fontsize=16,color="magenta"];229 -> 883[label="",style="dashed", color="magenta", weight=3];
229 -> 884[label="",style="dashed", color="magenta", weight=3];
1159[label="vuz56",fontsize=16,color="green",shape="box"];230 -> 899[label="",style="dashed", color="red", weight=0];
230[label="vuz7 * vuz7",fontsize=16,color="magenta"];230 -> 900[label="",style="dashed", color="magenta", weight=3];
230 -> 901[label="",style="dashed", color="magenta", weight=3];
1160[label="vuz56",fontsize=16,color="green",shape="box"];231 -> 913[label="",style="dashed", color="red", weight=0];
231[label="vuz7 * vuz7",fontsize=16,color="magenta"];231 -> 914[label="",style="dashed", color="magenta", weight=3];
231 -> 915[label="",style="dashed", color="magenta", weight=3];
1161[label="vuz56\n  Integral a",fontsize=16,color="green",shape="box"];232 -> 930[label="",style="dashed", color="red", weight=0];
232[label="vuz7 * vuz7\n  Integral a",fontsize=16,color="magenta"];232 -> 931[label="",style="dashed", color="magenta", weight=3];
232 -> 932[label="",style="dashed", color="magenta", weight=3];
1162[label="vuz56",fontsize=16,color="green",shape="box"];233 -> 944[label="",style="dashed", color="red", weight=0];
233[label="vuz7 * vuz7",fontsize=16,color="magenta"];233 -> 945[label="",style="dashed", color="magenta", weight=3];
233 -> 946[label="",style="dashed", color="magenta", weight=3];
1984 -> 2017[label="",style="dashed", color="red", weight=0];
1984[label="pr2F0G1 (vuz89 * vuz90) vuz89 (Pos (Succ vuz880)) (primEvenNat (Succ vuz880))\n  Num a",fontsize=16,color="magenta"];1984 -> 2018[label="",style="dashed", color="magenta", weight=3];
1984 -> 2019[label="",style="dashed", color="magenta", weight=3];
1984 -> 2020[label="",style="dashed", color="magenta", weight=3];
1984 -> 2021[label="",style="dashed", color="magenta", weight=3];
939[label="primMulFloat (Float vuz150 vuz151) (Float vuz500 vuz501)",fontsize=16,color="black",shape="box"];939 -> 953[label="",style="solid", color="black", weight=3];
1369[label="primDivNatS0 (Succ vuz570000) (Succ Zero) (primGEqNatS vuz570000 Zero)",fontsize=16,color="burlywood",shape="box"];2187[label="vuz570000/Succ vuz5700000",fontsize=10,color="white",style="solid",shape="box"];1369 -> 2187[label="",style="solid", color="burlywood", weight=9];
2187 -> 1379[label="",style="solid", color="burlywood", weight=3];
2188[label="vuz570000/Zero",fontsize=10,color="white",style="solid",shape="box"];1369 -> 2188[label="",style="solid", color="burlywood", weight=9];
2188 -> 1380[label="",style="solid", color="burlywood", weight=3];
1370[label="primDivNatS0 Zero (Succ Zero) False",fontsize=16,color="black",shape="box"];1370 -> 1381[label="",style="solid", color="black", weight=3];
1371[label="pr2F0G0 vuz68 (vuz69 * vuz69) (Pos (Succ vuz70)) True\n  Num a",fontsize=16,color="black",shape="box"];1371 -> 1382[label="",style="solid", color="black", weight=3];
1372[label="pr2F0G1 vuz68 (vuz69 * vuz69 * (vuz69 * vuz69)) (Pos (Succ vuz70) `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos (Succ vuz70) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1372 -> 1383[label="",style="solid", color="black", weight=3];
883[label="vuz7",fontsize=16,color="green",shape="box"];884[label="vuz7",fontsize=16,color="green",shape="box"];900[label="vuz7",fontsize=16,color="green",shape="box"];901[label="vuz7",fontsize=16,color="green",shape="box"];914[label="vuz7",fontsize=16,color="green",shape="box"];915[label="vuz7",fontsize=16,color="green",shape="box"];931[label="vuz7\n  Integral a",fontsize=16,color="green",shape="box"];932[label="vuz7\n  Integral a",fontsize=16,color="green",shape="box"];945[label="vuz7",fontsize=16,color="green",shape="box"];946[label="vuz7",fontsize=16,color="green",shape="box"];2018[label="vuz880",fontsize=16,color="green",shape="box"];2019[label="vuz90\n  Num a",fontsize=16,color="green",shape="box"];2020[label="vuz89\n  Num a",fontsize=16,color="green",shape="box"];2021[label="Succ vuz880",fontsize=16,color="green",shape="box"];2017[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) (primEvenNat vuz95)\n  Num a",fontsize=16,color="burlywood",shape="triangle"];2189[label="vuz95/Succ vuz950",fontsize=10,color="white",style="solid",shape="box"];2017 -> 2189[label="",style="solid", color="burlywood", weight=9];
2189 -> 2034[label="",style="solid", color="burlywood", weight=3];
2190[label="vuz95/Zero",fontsize=10,color="white",style="solid",shape="box"];2017 -> 2190[label="",style="solid", color="burlywood", weight=9];
2190 -> 2035[label="",style="solid", color="burlywood", weight=3];
953[label="Float (vuz150 * vuz500) (vuz151 * vuz501)",fontsize=16,color="green",shape="box"];953 -> 983[label="",style="dashed", color="green", weight=3];
953 -> 984[label="",style="dashed", color="green", weight=3];
1379[label="primDivNatS0 (Succ (Succ vuz5700000)) (Succ Zero) (primGEqNatS (Succ vuz5700000) Zero)",fontsize=16,color="black",shape="box"];1379 -> 1395[label="",style="solid", color="black", weight=3];
1380[label="primDivNatS0 (Succ Zero) (Succ Zero) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];1380 -> 1396[label="",style="solid", color="black", weight=3];
1381[label="Zero",fontsize=16,color="green",shape="box"];1382[label="pr2F (vuz69 * vuz69) (Pos (Succ vuz70) - fromInt (Pos (Succ Zero))) (vuz69 * vuz69 * vuz68)\n  Num a",fontsize=16,color="black",shape="box"];1382 -> 1397[label="",style="solid", color="black", weight=3];
1383[label="pr2F0G1 vuz68 (vuz69 * vuz69 * (vuz69 * vuz69)) (Pos (Succ vuz70) `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos (Succ vuz70) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1383 -> 1398[label="",style="solid", color="black", weight=3];
2034[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) (primEvenNat (Succ vuz950))\n  Num a",fontsize=16,color="burlywood",shape="box"];2191[label="vuz950/Succ vuz9500",fontsize=10,color="white",style="solid",shape="box"];2034 -> 2191[label="",style="solid", color="burlywood", weight=9];
2191 -> 2036[label="",style="solid", color="burlywood", weight=3];
2192[label="vuz950/Zero",fontsize=10,color="white",style="solid",shape="box"];2034 -> 2192[label="",style="solid", color="burlywood", weight=9];
2192 -> 2037[label="",style="solid", color="burlywood", weight=3];
2035[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="box"];2035 -> 2038[label="",style="solid", color="black", weight=3];
983 -> 878[label="",style="dashed", color="red", weight=0];
983[label="vuz150 * vuz500",fontsize=16,color="magenta"];983 -> 1024[label="",style="dashed", color="magenta", weight=3];
983 -> 1025[label="",style="dashed", color="magenta", weight=3];
984 -> 878[label="",style="dashed", color="red", weight=0];
984[label="vuz151 * vuz501",fontsize=16,color="magenta"];984 -> 1026[label="",style="dashed", color="magenta", weight=3];
984 -> 1027[label="",style="dashed", color="magenta", weight=3];
1395[label="primDivNatS0 (Succ (Succ vuz5700000)) (Succ Zero) True",fontsize=16,color="black",shape="box"];1395 -> 1410[label="",style="solid", color="black", weight=3];
1396[label="primDivNatS0 (Succ Zero) (Succ Zero) True",fontsize=16,color="black",shape="box"];1396 -> 1411[label="",style="solid", color="black", weight=3];
1397[label="pr2F4 (vuz69 * vuz69) (Pos (Succ vuz70) - fromInt (Pos (Succ Zero))) (vuz69 * vuz69 * vuz68)\n  Num a",fontsize=16,color="black",shape="box"];1397 -> 1412[label="",style="solid", color="black", weight=3];
1398[label="pr2F0G1 vuz68 (vuz69 * vuz69 * (vuz69 * vuz69)) (primQuotInt (Pos (Succ vuz70)) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos (Succ vuz70)) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="black",shape="box"];1398 -> 1413[label="",style="solid", color="black", weight=3];
2036[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) (primEvenNat (Succ (Succ vuz9500)))\n  Num a",fontsize=16,color="black",shape="box"];2036 -> 2039[label="",style="solid", color="black", weight=3];
2037[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) (primEvenNat (Succ Zero))\n  Num a",fontsize=16,color="black",shape="box"];2037 -> 2040[label="",style="solid", color="black", weight=3];
2038[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) True\n  Num a",fontsize=16,color="black",shape="box"];2038 -> 2041[label="",style="solid", color="black", weight=3];
1024[label="vuz150",fontsize=16,color="green",shape="box"];1025[label="vuz500",fontsize=16,color="green",shape="box"];1026[label="vuz151",fontsize=16,color="green",shape="box"];1027[label="vuz501",fontsize=16,color="green",shape="box"];1410[label="Succ (primDivNatS (primMinusNatS (Succ (Succ vuz5700000)) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1410 -> 1420[label="",style="dashed", color="green", weight=3];
1411[label="Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1411 -> 1421[label="",style="dashed", color="green", weight=3];
1412[label="pr2F3 (Pos (Succ vuz70) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) (vuz69 * vuz69) (Pos (Succ vuz70) - fromInt (Pos (Succ Zero))) (vuz69 * vuz69 * vuz68)\n  Num a",fontsize=16,color="black",shape="box"];1412 -> 1422[label="",style="solid", color="black", weight=3];
1413 -> 997[label="",style="dashed", color="red", weight=0];
1413[label="pr2F0G1 vuz68 (vuz69 * vuz69 * (vuz69 * vuz69)) (primQuotInt (Pos (Succ vuz70)) (Pos (Succ (Succ Zero)))) (primEvenInt (primQuotInt (Pos (Succ vuz70)) (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];1413 -> 1423[label="",style="dashed", color="magenta", weight=3];
1413 -> 1424[label="",style="dashed", color="magenta", weight=3];
1413 -> 1425[label="",style="dashed", color="magenta", weight=3];
2039 -> 2017[label="",style="dashed", color="red", weight=0];
2039[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) (primEvenNat vuz9500)\n  Num a",fontsize=16,color="magenta"];2039 -> 2042[label="",style="dashed", color="magenta", weight=3];
2040[label="pr2F0G1 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) False\n  Num a",fontsize=16,color="black",shape="box"];2040 -> 2043[label="",style="solid", color="black", weight=3];
2041[label="pr2F0G (vuz92 * vuz93) (vuz92 * vuz92) (Pos (Succ vuz94) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];2041 -> 2044[label="",style="solid", color="black", weight=3];
1420 -> 1318[label="",style="dashed", color="red", weight=0];
1420[label="primDivNatS (primMinusNatS (Succ (Succ vuz5700000)) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1420 -> 1427[label="",style="dashed", color="magenta", weight=3];
1421 -> 1322[label="",style="dashed", color="red", weight=0];
1421[label="primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1422 -> 1919[label="",style="dashed", color="red", weight=0];
1422[label="pr2F3 (primEqInt (Pos (Succ vuz70) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) (vuz69 * vuz69) (Pos (Succ vuz70) - fromInt (Pos (Succ Zero))) (vuz69 * vuz69 * vuz68)\n  Num a",fontsize=16,color="magenta"];1422 -> 1923[label="",style="dashed", color="magenta", weight=3];
1422 -> 1924[label="",style="dashed", color="magenta", weight=3];
1422 -> 1925[label="",style="dashed", color="magenta", weight=3];
1423[label="vuz69 * vuz69\n  Num a",fontsize=16,color="blue",shape="box"];2200[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1423 -> 2200[label="",style="solid", color="blue", weight=9];
2200 -> 1429[label="",style="solid", color="blue", weight=3];
2201[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1423 -> 2201[label="",style="solid", color="blue", weight=9];
2201 -> 1430[label="",style="solid", color="blue", weight=3];
2202[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1423 -> 2202[label="",style="solid", color="blue", weight=9];
2202 -> 1431[label="",style="solid", color="blue", weight=3];
2203[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1423 -> 2203[label="",style="solid", color="blue", weight=9];
2203 -> 1432[label="",style="solid", color="blue", weight=3];
2204[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1423 -> 2204[label="",style="solid", color="blue", weight=9];
2204 -> 1433[label="",style="solid", color="blue", weight=3];
1424[label="vuz68\n  Num a",fontsize=16,color="green",shape="box"];1425[label="Succ vuz70",fontsize=16,color="green",shape="box"];2042[label="vuz9500",fontsize=16,color="green",shape="box"];2043[label="pr2F0G0 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) otherwise\n  Num a",fontsize=16,color="black",shape="box"];2043 -> 2045[label="",style="solid", color="black", weight=3];
2044[label="pr2F0G2 (vuz92 * vuz93) (vuz92 * vuz92) (Pos (Succ vuz94) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];2044 -> 2046[label="",style="solid", color="black", weight=3];
1427[label="vuz5700000",fontsize=16,color="green",shape="box"];1923[label="vuz69 * vuz69\n  Num a",fontsize=16,color="blue",shape="box"];2205[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1923 -> 2205[label="",style="solid", color="blue", weight=9];
2205 -> 1942[label="",style="solid", color="blue", weight=3];
2206[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1923 -> 2206[label="",style="solid", color="blue", weight=9];
2206 -> 1943[label="",style="solid", color="blue", weight=3];
2207[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1923 -> 2207[label="",style="solid", color="blue", weight=9];
2207 -> 1944[label="",style="solid", color="blue", weight=3];
2208[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1923 -> 2208[label="",style="solid", color="blue", weight=9];
2208 -> 1945[label="",style="solid", color="blue", weight=3];
2209[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1923 -> 2209[label="",style="solid", color="blue", weight=9];
2209 -> 1946[label="",style="solid", color="blue", weight=3];
1924[label="vuz70",fontsize=16,color="green",shape="box"];1925[label="vuz68\n  Num a",fontsize=16,color="green",shape="box"];1429 -> 229[label="",style="dashed", color="red", weight=0];
1429[label="vuz69 * vuz69",fontsize=16,color="magenta"];1429 -> 1437[label="",style="dashed", color="magenta", weight=3];
1430 -> 230[label="",style="dashed", color="red", weight=0];
1430[label="vuz69 * vuz69",fontsize=16,color="magenta"];1430 -> 1438[label="",style="dashed", color="magenta", weight=3];
1431 -> 231[label="",style="dashed", color="red", weight=0];
1431[label="vuz69 * vuz69",fontsize=16,color="magenta"];1431 -> 1439[label="",style="dashed", color="magenta", weight=3];
1432 -> 232[label="",style="dashed", color="red", weight=0];
1432[label="vuz69 * vuz69\n  Integral a",fontsize=16,color="magenta"];1432 -> 1440[label="",style="dashed", color="magenta", weight=3];
1433 -> 233[label="",style="dashed", color="red", weight=0];
1433[label="vuz69 * vuz69",fontsize=16,color="magenta"];1433 -> 1441[label="",style="dashed", color="magenta", weight=3];
2045[label="pr2F0G0 (vuz92 * vuz93) vuz92 (Pos (Succ vuz94)) True\n  Num a",fontsize=16,color="black",shape="box"];2045 -> 2047[label="",style="solid", color="black", weight=3];
2046[label="pr2F0G1 (vuz92 * vuz93) (vuz92 * vuz92) (Pos (Succ vuz94) `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos (Succ vuz94) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];2046 -> 2048[label="",style="solid", color="black", weight=3];
1942 -> 229[label="",style="dashed", color="red", weight=0];
1942[label="vuz69 * vuz69",fontsize=16,color="magenta"];1942 -> 1948[label="",style="dashed", color="magenta", weight=3];
1943 -> 230[label="",style="dashed", color="red", weight=0];
1943[label="vuz69 * vuz69",fontsize=16,color="magenta"];1943 -> 1949[label="",style="dashed", color="magenta", weight=3];
1944 -> 231[label="",style="dashed", color="red", weight=0];
1944[label="vuz69 * vuz69",fontsize=16,color="magenta"];1944 -> 1950[label="",style="dashed", color="magenta", weight=3];
1945 -> 232[label="",style="dashed", color="red", weight=0];
1945[label="vuz69 * vuz69\n  Integral a",fontsize=16,color="magenta"];1945 -> 1951[label="",style="dashed", color="magenta", weight=3];
1946 -> 233[label="",style="dashed", color="red", weight=0];
1946[label="vuz69 * vuz69",fontsize=16,color="magenta"];1946 -> 1952[label="",style="dashed", color="magenta", weight=3];
1437[label="vuz69",fontsize=16,color="green",shape="box"];1438[label="vuz69",fontsize=16,color="green",shape="box"];1439[label="vuz69",fontsize=16,color="green",shape="box"];1440[label="vuz69\n  Integral a",fontsize=16,color="green",shape="box"];1441[label="vuz69",fontsize=16,color="green",shape="box"];2047[label="pr2F vuz92 (Pos (Succ vuz94) - fromInt (Pos (Succ Zero))) (vuz92 * (vuz92 * vuz93))\n  Num a",fontsize=16,color="black",shape="box"];2047 -> 2049[label="",style="solid", color="black", weight=3];
2048[label="pr2F0G1 (vuz92 * vuz93) (vuz92 * vuz92) (Pos (Succ vuz94) `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos (Succ vuz94) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];2048 -> 2050[label="",style="solid", color="black", weight=3];
1948[label="vuz69",fontsize=16,color="green",shape="box"];1949[label="vuz69",fontsize=16,color="green",shape="box"];1950[label="vuz69",fontsize=16,color="green",shape="box"];1951[label="vuz69\n  Integral a",fontsize=16,color="green",shape="box"];1952[label="vuz69",fontsize=16,color="green",shape="box"];2049[label="pr2F4 vuz92 (Pos (Succ vuz94) - fromInt (Pos (Succ Zero))) (vuz92 * (vuz92 * vuz93))\n  Num a",fontsize=16,color="black",shape="box"];2049 -> 2051[label="",style="solid", color="black", weight=3];
2050[label="pr2F0G1 (vuz92 * vuz93) (vuz92 * vuz92) (primQuotInt (Pos (Succ vuz94)) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos (Succ vuz94)) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="black",shape="box"];2050 -> 2052[label="",style="solid", color="black", weight=3];
2051[label="pr2F3 (Pos (Succ vuz94) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) vuz92 (Pos (Succ vuz94) - fromInt (Pos (Succ Zero))) (vuz92 * (vuz92 * vuz93))\n  Num a",fontsize=16,color="black",shape="box"];2051 -> 2053[label="",style="solid", color="black", weight=3];
2052 -> 997[label="",style="dashed", color="red", weight=0];
2052[label="pr2F0G1 (vuz92 * vuz93) (vuz92 * vuz92) (primQuotInt (Pos (Succ vuz94)) (Pos (Succ (Succ Zero)))) (primEvenInt (primQuotInt (Pos (Succ vuz94)) (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];2052 -> 2054[label="",style="dashed", color="magenta", weight=3];
2052 -> 2055[label="",style="dashed", color="magenta", weight=3];
2052 -> 2056[label="",style="dashed", color="magenta", weight=3];
2053 -> 1919[label="",style="dashed", color="red", weight=0];
2053[label="pr2F3 (primEqInt (Pos (Succ vuz94) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz92 (Pos (Succ vuz94) - fromInt (Pos (Succ Zero))) (vuz92 * (vuz92 * vuz93))\n  Num a",fontsize=16,color="magenta"];2053 -> 2057[label="",style="dashed", color="magenta", weight=3];
2053 -> 2058[label="",style="dashed", color="magenta", weight=3];
2053 -> 2059[label="",style="dashed", color="magenta", weight=3];
2054[label="vuz92\n  Num a",fontsize=16,color="green",shape="box"];2055[label="vuz92 * vuz93\n  Num a",fontsize=16,color="blue",shape="box"];2222[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2055 -> 2222[label="",style="solid", color="blue", weight=9];
2222 -> 2060[label="",style="solid", color="blue", weight=3];
2223[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];2055 -> 2223[label="",style="solid", color="blue", weight=9];
2223 -> 2061[label="",style="solid", color="blue", weight=3];
2224[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];2055 -> 2224[label="",style="solid", color="blue", weight=9];
2224 -> 2062[label="",style="solid", color="blue", weight=3];
2225[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];2055 -> 2225[label="",style="solid", color="blue", weight=9];
2225 -> 2063[label="",style="solid", color="blue", weight=3];
2226[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];2055 -> 2226[label="",style="solid", color="blue", weight=9];
2226 -> 2064[label="",style="solid", color="blue", weight=3];
2056[label="Succ vuz94",fontsize=16,color="green",shape="box"];2057[label="vuz92\n  Num a",fontsize=16,color="green",shape="box"];2058[label="vuz94",fontsize=16,color="green",shape="box"];2059[label="vuz92 * vuz93\n  Num a",fontsize=16,color="blue",shape="box"];2227[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2059 -> 2227[label="",style="solid", color="blue", weight=9];
2227 -> 2065[label="",style="solid", color="blue", weight=3];
2228[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];2059 -> 2228[label="",style="solid", color="blue", weight=9];
2228 -> 2066[label="",style="solid", color="blue", weight=3];
2229[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];2059 -> 2229[label="",style="solid", color="blue", weight=9];
2229 -> 2067[label="",style="solid", color="blue", weight=3];
2230[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];2059 -> 2230[label="",style="solid", color="blue", weight=9];
2230 -> 2068[label="",style="solid", color="blue", weight=3];
2231[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];2059 -> 2231[label="",style="solid", color="blue", weight=9];
2231 -> 2069[label="",style="solid", color="blue", weight=3];
2060 -> 878[label="",style="dashed", color="red", weight=0];
2060[label="vuz92 * vuz93",fontsize=16,color="magenta"];2060 -> 2070[label="",style="dashed", color="magenta", weight=3];
2060 -> 2071[label="",style="dashed", color="magenta", weight=3];
2061 -> 899[label="",style="dashed", color="red", weight=0];
2061[label="vuz92 * vuz93",fontsize=16,color="magenta"];2061 -> 2072[label="",style="dashed", color="magenta", weight=3];
2061 -> 2073[label="",style="dashed", color="magenta", weight=3];
2062 -> 913[label="",style="dashed", color="red", weight=0];
2062[label="vuz92 * vuz93",fontsize=16,color="magenta"];2062 -> 2074[label="",style="dashed", color="magenta", weight=3];
2062 -> 2075[label="",style="dashed", color="magenta", weight=3];
2063 -> 930[label="",style="dashed", color="red", weight=0];
2063[label="vuz92 * vuz93\n  Integral a",fontsize=16,color="magenta"];2063 -> 2076[label="",style="dashed", color="magenta", weight=3];
2063 -> 2077[label="",style="dashed", color="magenta", weight=3];
2064 -> 944[label="",style="dashed", color="red", weight=0];
2064[label="vuz92 * vuz93",fontsize=16,color="magenta"];2064 -> 2078[label="",style="dashed", color="magenta", weight=3];
2064 -> 2079[label="",style="dashed", color="magenta", weight=3];
2065 -> 878[label="",style="dashed", color="red", weight=0];
2065[label="vuz92 * vuz93",fontsize=16,color="magenta"];2065 -> 2080[label="",style="dashed", color="magenta", weight=3];
2065 -> 2081[label="",style="dashed", color="magenta", weight=3];
2066 -> 899[label="",style="dashed", color="red", weight=0];
2066[label="vuz92 * vuz93",fontsize=16,color="magenta"];2066 -> 2082[label="",style="dashed", color="magenta", weight=3];
2066 -> 2083[label="",style="dashed", color="magenta", weight=3];
2067 -> 913[label="",style="dashed", color="red", weight=0];
2067[label="vuz92 * vuz93",fontsize=16,color="magenta"];2067 -> 2084[label="",style="dashed", color="magenta", weight=3];
2067 -> 2085[label="",style="dashed", color="magenta", weight=3];
2068 -> 930[label="",style="dashed", color="red", weight=0];
2068[label="vuz92 * vuz93\n  Integral a",fontsize=16,color="magenta"];2068 -> 2086[label="",style="dashed", color="magenta", weight=3];
2068 -> 2087[label="",style="dashed", color="magenta", weight=3];
2069 -> 944[label="",style="dashed", color="red", weight=0];
2069[label="vuz92 * vuz93",fontsize=16,color="magenta"];2069 -> 2088[label="",style="dashed", color="magenta", weight=3];
2069 -> 2089[label="",style="dashed", color="magenta", weight=3];
2070[label="vuz92",fontsize=16,color="green",shape="box"];2071[label="vuz93",fontsize=16,color="green",shape="box"];2072[label="vuz92",fontsize=16,color="green",shape="box"];2073[label="vuz93",fontsize=16,color="green",shape="box"];2074[label="vuz93",fontsize=16,color="green",shape="box"];2075[label="vuz92",fontsize=16,color="green",shape="box"];2076[label="vuz93\n  Integral a",fontsize=16,color="green",shape="box"];2077[label="vuz92\n  Integral a",fontsize=16,color="green",shape="box"];2078[label="vuz92",fontsize=16,color="green",shape="box"];2079[label="vuz93",fontsize=16,color="green",shape="box"];2080[label="vuz92",fontsize=16,color="green",shape="box"];2081[label="vuz93",fontsize=16,color="green",shape="box"];2082[label="vuz92",fontsize=16,color="green",shape="box"];2083[label="vuz93",fontsize=16,color="green",shape="box"];2084[label="vuz93",fontsize=16,color="green",shape="box"];2085[label="vuz92",fontsize=16,color="green",shape="box"];2086[label="vuz93\n  Integral a",fontsize=16,color="green",shape="box"];2087[label="vuz92\n  Integral a",fontsize=16,color="green",shape="box"];2088[label="vuz92",fontsize=16,color="green",shape="box"];2089[label="vuz93",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuz5700000))) → new_primDivNatS(vuz5700000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS(Succ(Succ(vuz5700000))) → new_primDivNatS(vuz5700000)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vuz5800), Succ(vuz49000)) → new_primPlusNat(vuz5800, vuz49000)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(vuz5800), Succ(vuz49000)) → new_primPlusNat(vuz5800, vuz49000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vuz1500), Succ(vuz4900)) → new_primMulNat(vuz1500, Succ(vuz4900))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(vuz1500), Succ(vuz4900)) → new_primMulNat(vuz1500, Succ(vuz4900))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G12(vuz55, vuz56, bc) → new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Zero), ba) → new_pr2F3(vuz94, vuz92, new_sr(vuz92, vuz93, ba), ba)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Succ(vuz57000))), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS0(vuz57000), Succ(new_primDivNatS0(vuz57000)), bc)
new_pr2F0G10(vuz55, vuz56, Zero, bc) → new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)
new_pr2F0G10(vuz55, vuz56, Succ(Zero), bc) → new_pr2F0G12(vuz55, vuz56, bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Zero), bd) → new_pr2F3(vuz70, new_sr2(vuz69, bd), vuz68, bd)

The TRS R consists of the following rules:

new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr8(vuz15, vuz53) → error([])
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_sr1(vuz56, ty_Int) → new_sr10(vuz56)
new_sr6(vuz15, vuz51) → error([])
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_primPlusNat1(Zero, Zero) → Zero
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_primDivNatS1 → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_sr1(vuz56, ty_Float) → new_sr13(vuz56)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr1(vuz56, ty_Integer) → new_sr11(vuz56)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primMulNat0(Zero, Zero) → Zero
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_sr1(vuz56, app(ty_Ratio, bg)) → new_sr12(vuz56, bg)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr1(vuz56, ty_Double) → new_sr9(vuz56)
new_primDivNatS0(Zero) → Zero
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr1(x0, app(ty_Ratio, x1))
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr1(x0, ty_Int)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_sr1(x0, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr1(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr1(x0, ty_Float)
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz55, vuz56, Zero, bc) → new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr8(vuz15, vuz53) → error([])
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_sr1(vuz56, ty_Int) → new_sr10(vuz56)
new_sr6(vuz15, vuz51) → error([])
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_primPlusNat1(Zero, Zero) → Zero
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_primDivNatS1 → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_sr1(vuz56, ty_Float) → new_sr13(vuz56)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr1(vuz56, ty_Integer) → new_sr11(vuz56)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primMulNat0(Zero, Zero) → Zero
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_sr1(vuz56, app(ty_Ratio, bg)) → new_sr12(vuz56, bg)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr1(vuz56, ty_Double) → new_sr9(vuz56)
new_primDivNatS0(Zero) → Zero
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr1(x0, app(ty_Ratio, x1))
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr1(x0, ty_Int)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_sr1(x0, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr1(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr1(x0, ty_Float)
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz55, vuz56, Zero, bc) → new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz56, ty_Int) → new_sr10(vuz56)
new_sr1(vuz56, ty_Float) → new_sr13(vuz56)
new_sr1(vuz56, ty_Integer) → new_sr11(vuz56)
new_sr1(vuz56, app(ty_Ratio, bg)) → new_sr12(vuz56, bg)
new_sr1(vuz56, ty_Double) → new_sr9(vuz56)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr6(vuz15, vuz51) → error([])
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr8(vuz15, vuz53) → error([])
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr1(x0, app(ty_Ratio, x1))
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr1(x0, ty_Int)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_sr1(x0, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr1(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr1(x0, ty_Float)
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr2(x0, ty_Integer)
new_sr2(x0, ty_Float)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Double)
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_sr3(x0, ty_Integer)
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ MNOCProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz55, vuz56, Zero, bc) → new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz56, ty_Int) → new_sr10(vuz56)
new_sr1(vuz56, ty_Float) → new_sr13(vuz56)
new_sr1(vuz56, ty_Integer) → new_sr11(vuz56)
new_sr1(vuz56, app(ty_Ratio, bg)) → new_sr12(vuz56, bg)
new_sr1(vuz56, ty_Double) → new_sr9(vuz56)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr6(vuz15, vuz51) → error([])
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr8(vuz15, vuz53) → error([])
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)

The set Q consists of the following terms:

new_sr8(x0, x1)
new_primMulNat0(Zero, Zero)
new_sr1(x0, app(ty_Ratio, x1))
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Zero)
new_sr1(x0, ty_Int)
new_sr1(x0, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_sr1(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr1(x0, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr9(x0)

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ MNOCProof

                                            ↳ QDP

                                              ↳ NonTerminationProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz55, vuz56, Zero, bc) → new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz56, ty_Int) → new_sr10(vuz56)
new_sr1(vuz56, ty_Float) → new_sr13(vuz56)
new_sr1(vuz56, ty_Integer) → new_sr11(vuz56)
new_sr1(vuz56, app(ty_Ratio, bg)) → new_sr12(vuz56, bg)
new_sr1(vuz56, ty_Double) → new_sr9(vuz56)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr6(vuz15, vuz51) → error([])
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr8(vuz15, vuz53) → error([])
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_pr2F0G10(vuz55, vuz56, Zero, bc) → new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz56, ty_Int) → new_sr10(vuz56)
new_sr1(vuz56, ty_Float) → new_sr13(vuz56)
new_sr1(vuz56, ty_Integer) → new_sr11(vuz56)
new_sr1(vuz56, app(ty_Ratio, bg)) → new_sr12(vuz56, bg)
new_sr1(vuz56, ty_Double) → new_sr9(vuz56)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr6(vuz15, vuz51) → error([])
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr8(vuz15, vuz53) → error([])
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)

s = new_pr2F0G10(vuz55, vuz56, Zero, bc) evaluates to t =new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [vuz56 / new_sr1(vuz56, bc)]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_pr2F0G10(vuz55, vuz56, Zero, bc) to new_pr2F0G10(vuz55, new_sr1(vuz56, bc), Zero, bc).

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Succ(vuz57000))), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS0(vuz57000), Succ(new_primDivNatS0(vuz57000)), bc)
new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Zero), ba) → new_pr2F3(vuz94, vuz92, new_sr(vuz92, vuz93, ba), ba)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Zero), bd) → new_pr2F3(vuz70, new_sr2(vuz69, bd), vuz68, bd)

The TRS R consists of the following rules:

new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr8(vuz15, vuz53) → error([])
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_sr1(vuz56, ty_Int) → new_sr10(vuz56)
new_sr6(vuz15, vuz51) → error([])
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_primPlusNat1(Zero, Zero) → Zero
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_primDivNatS1 → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_sr1(vuz56, ty_Float) → new_sr13(vuz56)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr1(vuz56, ty_Integer) → new_sr11(vuz56)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primMulNat0(Zero, Zero) → Zero
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_sr1(vuz56, app(ty_Ratio, bg)) → new_sr12(vuz56, bg)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr1(vuz56, ty_Double) → new_sr9(vuz56)
new_primDivNatS0(Zero) → Zero
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr1(x0, app(ty_Ratio, x1))
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr1(x0, ty_Int)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_sr1(x0, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr1(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr1(x0, ty_Float)
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Succ(vuz57000))), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS0(vuz57000), Succ(new_primDivNatS0(vuz57000)), bc)
new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Zero), ba) → new_pr2F3(vuz94, vuz92, new_sr(vuz92, vuz93, ba), ba)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Zero), bd) → new_pr2F3(vuz70, new_sr2(vuz69, bd), vuz68, bd)

The TRS R consists of the following rules:

new_primDivNatS1 → Zero
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr6(vuz15, vuz51) → error([])
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr8(vuz15, vuz53) → error([])
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr1(x0, app(ty_Ratio, x1))
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr1(x0, ty_Int)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_sr1(x0, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr1(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr1(x0, ty_Float)
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr1(x0, app(ty_Ratio, x1))
new_sr1(x0, ty_Int)
new_sr1(x0, ty_Integer)
new_sr1(x0, ty_Double)
new_sr1(x0, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Zero), ba) → new_pr2F3(vuz94, vuz92, new_sr(vuz92, vuz93, ba), ba)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Succ(vuz57000))), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS0(vuz57000), Succ(new_primDivNatS0(vuz57000)), bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Zero), bd) → new_pr2F3(vuz70, new_sr2(vuz69, bd), vuz68, bd)

The TRS R consists of the following rules:

new_primDivNatS1 → Zero
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr6(vuz15, vuz51) → error([])
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr8(vuz15, vuz53) → error([])
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS1, Succ(new_primDivNatS1), bc) at position [2] we obtained the following new rules:

new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, Zero, Succ(new_primDivNatS1), bc)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, Zero, Succ(new_primDivNatS1), bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Succ(vuz57000))), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS0(vuz57000), Succ(new_primDivNatS0(vuz57000)), bc)
new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Zero), ba) → new_pr2F3(vuz94, vuz92, new_sr(vuz92, vuz93, ba), ba)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Zero), bd) → new_pr2F3(vuz70, new_sr2(vuz69, bd), vuz68, bd)

The TRS R consists of the following rules:

new_primDivNatS1 → Zero
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr6(vuz15, vuz51) → error([])
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr8(vuz15, vuz53) → error([])
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, Zero, Succ(new_primDivNatS1), bc) at position [3,0] we obtained the following new rules:

new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, Zero, Succ(Zero), bc)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, Zero, Succ(Zero), bc)
new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Zero), ba) → new_pr2F3(vuz94, vuz92, new_sr(vuz92, vuz93, ba), ba)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Succ(vuz57000))), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS0(vuz57000), Succ(new_primDivNatS0(vuz57000)), bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Zero), bd) → new_pr2F3(vuz70, new_sr2(vuz69, bd), vuz68, bd)

The TRS R consists of the following rules:

new_primDivNatS1 → Zero
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr6(vuz15, vuz51) → error([])
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr8(vuz15, vuz53) → error([])
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_pr2F0G10(vuz55, vuz56, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz55, vuz56, Zero, Succ(Zero), bc)
new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Zero), ba) → new_pr2F3(vuz94, vuz92, new_sr(vuz92, vuz93, ba), ba)
new_pr2F0G10(vuz55, vuz56, Succ(Succ(Succ(vuz57000))), bc) → new_pr2F0G11(vuz55, vuz56, new_primDivNatS0(vuz57000), Succ(new_primDivNatS0(vuz57000)), bc)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Zero), bd) → new_pr2F3(vuz70, new_sr2(vuz69, bd), vuz68, bd)

The remaining pairs can at least be oriented weakly.

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)

Used ordering: Polynomial interpretation [25]:

POL(Float(x₁, x₂)) = 0
POL(Neg(x₁)) = 1 + x₁
POL(Pos(x₁)) = 1 + x₁
POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL([]) = 0
POL(app(x₁, x₂)) = 1 + x₁ + x₂
POL(error(x₁)) = 0
POL(new_pr2F0G1(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃
POL(new_pr2F0G10(x₁, x₂, x₃, x₄)) = x₃
POL(new_pr2F0G11(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃
POL(new_pr2F3(x₁, x₂, x₃, x₄)) = x₁
POL(new_primDivNatS0(x₁)) = x₁
POL(new_primDivNatS1) = 0
POL(new_primMulNat0(x₁, x₂)) = 0
POL(new_primPlusNat0(x₁, x₂)) = 0
POL(new_primPlusNat1(x₁, x₂)) = 1 + x₁ + x₂
POL(new_sr(x₁, x₂, x₃)) = 0
POL(new_sr0(x₁, x₂, x₃)) = 0
POL(new_sr10(x₁)) = 1 + x₁
POL(new_sr11(x₁)) = 1 + x₁
POL(new_sr12(x₁, x₂)) = 1
POL(new_sr13(x₁)) = 0
POL(new_sr2(x₁, x₂)) = x₁ + x₂
POL(new_sr3(x₁, x₂)) = 0
POL(new_sr4(x₁, x₂)) = 1 + x₂
POL(new_sr5(x₁, x₂)) = 0
POL(new_sr6(x₁, x₂)) = x₁
POL(new_sr7(x₁, x₂, x₃)) = 0
POL(new_sr8(x₁, x₂)) = 0
POL(new_sr9(x₁)) = x₁
POL(ty_Double) = 0
POL(ty_Float) = 0
POL(ty_Int) = 1
POL(ty_Integer) = 1
POL(ty_Ratio) = 1

The following usable rules [17] were oriented:

new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
new_pr2F3(Succ(vuz880), vuz89, vuz90, bb) → new_pr2F0G1(vuz89, vuz90, vuz880, Succ(vuz880), bb)
new_pr2F0G11(vuz68, vuz69, vuz70, Zero, bd) → new_pr2F0G10(vuz68, new_sr3(vuz69, bd), Succ(vuz70), bd)
new_pr2F0G1(vuz92, vuz93, vuz94, Zero, ba) → new_pr2F0G10(new_sr0(vuz92, vuz93, ba), vuz92, Succ(vuz94), ba)
new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)

The TRS R consists of the following rules:

new_primDivNatS1 → Zero
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr6(vuz15, vuz51) → error([])
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr8(vuz15, vuz53) → error([])
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 3 less nodes.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)

The TRS R consists of the following rules:

new_primDivNatS1 → Zero
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr6(vuz15, vuz51) → error([])
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr8(vuz15, vuz53) → error([])
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)

R is empty.
The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                                  ↳ QDP

                                                                    ↳ QDPSizeChangeProof

                                                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)

From the DPs we obtained the following set of size-change graphs:

new_pr2F0G11(vuz68, vuz69, vuz70, Succ(Succ(vuz7100)), bd) → new_pr2F0G11(vuz68, vuz69, vuz70, vuz7100, bd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)

The TRS R consists of the following rules:

new_primDivNatS1 → Zero
new_sr0(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr0(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr0(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr0(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr6(vuz15, vuz51) → error([])
new_sr4(Pos(vuz150), Neg(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Pos(vuz490)) → Neg(new_primMulNat0(vuz150, vuz490))
new_sr4(Neg(vuz150), Neg(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_sr4(Pos(vuz150), Pos(vuz490)) → Pos(new_primMulNat0(vuz150, vuz490))
new_primMulNat0(Zero, Succ(vuz4900)) → Zero
new_primMulNat0(Succ(vuz1500), Zero) → Zero
new_primMulNat0(Succ(vuz1500), Succ(vuz4900)) → new_primPlusNat0(new_primMulNat0(vuz1500, Succ(vuz4900)), vuz4900)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz580), vuz4900) → Succ(Succ(new_primPlusNat1(vuz580, vuz4900)))
new_primPlusNat0(Zero, vuz4900) → Succ(vuz4900)
new_primPlusNat1(Succ(vuz5800), Succ(vuz49000)) → Succ(Succ(new_primPlusNat1(vuz5800, vuz49000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz49000)) → Succ(vuz49000)
new_primPlusNat1(Succ(vuz5800), Zero) → Succ(vuz5800)
new_sr7(vuz15, vuz52, ca) → error([])
new_sr8(vuz15, vuz53) → error([])
new_sr5(Float(vuz150, vuz151), Float(vuz500, vuz501)) → Float(new_sr4(vuz150, vuz500), new_sr4(vuz151, vuz501))
new_sr(vuz92, vuz93, app(ty_Ratio, be)) → new_sr7(vuz92, vuz93, be)
new_sr(vuz92, vuz93, ty_Integer) → new_sr8(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Double) → new_sr6(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Int) → new_sr4(vuz92, vuz93)
new_sr(vuz92, vuz93, ty_Float) → new_sr5(vuz92, vuz93)
new_sr2(vuz69, ty_Int) → new_sr10(vuz69)
new_sr2(vuz69, ty_Double) → new_sr9(vuz69)
new_sr2(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr2(vuz69, ty_Float) → new_sr13(vuz69)
new_sr2(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr12(vuz7, bf) → new_sr7(vuz7, vuz7, bf)
new_sr13(vuz7) → new_sr5(vuz7, vuz7)
new_sr11(vuz7) → new_sr8(vuz7, vuz7)
new_sr9(vuz7) → new_sr6(vuz7, vuz7)
new_sr10(vuz7) → new_sr4(vuz7, vuz7)
new_sr3(vuz69, ty_Integer) → new_sr11(vuz69)
new_sr3(vuz69, ty_Int) → new_sr10(vuz69)
new_sr3(vuz69, app(ty_Ratio, bh)) → new_sr12(vuz69, bh)
new_sr3(vuz69, ty_Float) → new_sr13(vuz69)
new_sr3(vuz69, ty_Double) → new_sr9(vuz69)
new_primDivNatS0(Succ(Succ(vuz5700000))) → Succ(new_primDivNatS0(vuz5700000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)

R is empty.
The set Q consists of the following terms:

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr8(x0, x1)
new_sr(x0, x1, ty_Integer)
new_sr0(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_sr2(x0, ty_Int)
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, ty_Double)
new_sr6(x0, x1)
new_sr11(x0)
new_sr13(x0)
new_sr3(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr4(Neg(x0), Neg(x1))
new_sr12(x0, x1)
new_primPlusNat0(Succ(x0), x1)
new_sr3(x0, ty_Double)
new_sr0(x0, x1, ty_Integer)
new_sr10(x0)
new_primPlusNat1(Zero, Zero)
new_primPlusNat1(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_sr2(x0, ty_Integer)
new_sr7(x0, x1, x2)
new_sr4(Neg(x0), Pos(x1))
new_sr4(Pos(x0), Neg(x1))
new_primPlusNat0(Zero, x0)
new_sr2(x0, ty_Float)
new_primMulNat0(Succ(x0), Zero)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr3(x0, app(ty_Ratio, x1))
new_sr0(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_sr2(x0, ty_Double)
new_sr4(Pos(x0), Pos(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_sr3(x0, ty_Int)
new_primDivNatS0(Succ(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr3(x0, ty_Integer)
new_sr5(Float(x0, x1), Float(x2, x3))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr9(x0)
new_sr(x0, x1, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                                  ↳ QDP

                                                                    ↳ QDPSizeChangeProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)

From the DPs we obtained the following set of size-change graphs:

new_pr2F0G1(vuz92, vuz93, vuz94, Succ(Succ(vuz9500)), ba) → new_pr2F0G1(vuz92, vuz93, vuz94, vuz9500, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G13(vuz7, vuz8, Succ(Succ(vuz900)), ba) → new_pr2F0G13(vuz7, vuz8, vuz900, ba)

From the DPs we obtained the following set of size-change graphs:

new_pr2F0G13(vuz7, vuz8, Succ(Succ(vuz900)), ba) → new_pr2F0G13(vuz7, vuz8, vuz900, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4

Haskell To QDPs

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

prPr0	x n True	= x ^ n
prPr0	x n False	= recip (x ^ (`negate` n))

g1	x n True	= g (x * x) (n `quot` 2)
g1	x n False	= g0 x n otherwise

pr2F4	vv yu y	= pr2F3 (yu == 0) vv yu y
pr2F4	yz zu zv	= pr2F0 yz zu zv

pr2F0G1	vuy x n True	= pr2F0G vuy (x * x) (n `quot` 2)
pr2F0G1	vuy x n False	= pr2F0G0 vuy x n otherwise